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

chore: remove old version

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-11 14:50:15 -08:00
parent 4e47ef0cbb
commit 0434c36f89
1 changed files with 0 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/WFTactics.lean
View file

@ -7,21 +7,6 @@ prelude
import Init.SizeOf
import Init.WF
macro "default_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
))
macro "decreasing_tactic" : tactic =>
`((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel];
repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)