From 093805f7f2bf7f7b5bfd17be30f050a3082cd8c9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 28 Jul 2020 15:19:36 +0100 Subject: [PATCH] feat(?): Better support for prod in well_founded --- library/init/meta/well_founded_tactics.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean index e31dbdbb7c..e97821c7b9 100644 --- a/library/init/meta/well_founded_tactics.lean +++ b/library/init/meta/well_founded_tactics.lean @@ -42,6 +42,10 @@ meta def is_psigma_mk : expr → tactic (expr × expr) | `(psigma.mk %%a %%b) := return (a, b) | _ := failed +meta def is_prod_mk : expr → tactic (expr × expr) +| `(prod.mk %%a %%b) := return (a, b) +| _ := failed + meta def process_lex : tactic unit → tactic unit | tac := do t ← target >>= whnf, @@ -53,6 +57,14 @@ meta def process_lex : tactic unit → tactic unit (is_def_eq a₁ b₁ >> `[apply psigma.lex.right] >> process_lex tac) <|> (`[apply psigma.lex.left] >> tac) + else if t.is_napp_of `prod.lex 6 then + let a := t.app_fn.app_arg in + let b := t.app_arg in + do (a₁, a₂) ← is_prod_mk a, + (b₁, b₂) ← is_prod_mk b, + (is_def_eq a₁ b₁ >> `[apply prod.lex.right] >> process_lex tac) + <|> + (`[apply prod.lex.left] >> tac) else tac