From 0434c36f89a3828b034e491cdda9f9f56cd5ba96 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Jan 2022 14:50:15 -0800 Subject: [PATCH] chore: remove old version --- src/Init/WFTactics.lean | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 1a5cc67a18..46b8551ed9 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -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)