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

feat: make decreasing_tactic easier to extend

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-19 08:42:38 -07:00
parent ef3143e1eb
commit c8c4d47420
1 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Init/WFTactics.lean
View file

@ -9,18 +9,22 @@ import Init.WF
macro "simp_wf" : tactic => `(simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
syntax "decreasing_tactic_trivial" : tactic -- Extensible helper tactic for `decreasing_tactic`
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| assumption)
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| decide) -- e.g., 0 < 1
macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.lt_succ_self) -- i < i+1
macro "decreasing_tactic" : tactic =>
`((simp_wf
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
| simp (config := { arith := true }); done
| decreasing_tactic_trivial
| fail "failed to prove termination, possible solutions:\n - Use `have`-expressions to prove the remaining goals\n - Use `termination_by` to specify a different well-founded relation\n - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"
-- TODO: linearith
-- TODO: improve