max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: prepare to rename default_decreasing_tactic

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-11 14:42:25 -08:00
parent 2464da0dca
commit ca89da28d0
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/WFTactics.lean
View file

@ -21,3 +21,18 @@ macro "default_decreasing_tactic" : tactic =>
-- TODO: linearith
-- TODO: improve
))
macro "decreasing_tactic" : tactic =>
`((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel];
repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
first
| apply Nat.lt_succ_self -- i < i+1
| decide -- e.g., 0 < 1
| apply Nat.pred_lt; assumption -- i-1 < i if i ≠ 0
| apply Nat.pred_lt'; assumption -- i-1 < i if j < i
| apply Nat.sub_succ_lt_self; assumption -- a - (i+1) < a - i if i < a
| assumption
-- TODO: linearith
-- TODO: improve
))