de23226d0c
Encouraged by the performance gains from making `rewrite` produce smaller proof objects (#3121) I am here looking for low-hanging fruit in `simp`. Consider this typical example: ``` set_option pp.explicit true theorem test (a : Nat) (b : Nat) (c : Nat) (heq : a = b) (h : (c.add (c.add ((c.add b).add c))).add c = c) : (c.add (c.add ((c.add a).add c))).add c = c ``` We get a rather nice proof term when using ``` := by rw [heq]; assumption ``` namely ``` theorem test : ∀ (a b c : Nat), @Eq Nat a b → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c := fun a b c heq h => @Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c) (@congrArg Nat Prop a b (fun _a => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c _a) c))) c) c) heq) h ``` (this is with #3121). But with `by simp only [heq]; assumption`, it looks rather different: ``` theorem test : ∀ (a b c : Nat), @Eq Nat a b → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c := fun a b c heq h => @Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c) (@id (@Eq Prop (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)) (@congrFun Nat (fun a => Prop) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c)) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c)) (@congrArg Nat (Nat → Prop) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) (@Eq Nat) (@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c)))) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c)))) (@congrArg Nat (Nat → Nat) (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) Nat.add (@congrArg Nat Nat (Nat.add c (Nat.add (Nat.add c a) c)) (Nat.add c (Nat.add (Nat.add c b) c)) (Nat.add c) (@congrArg Nat Nat (Nat.add (Nat.add c a) c) (Nat.add (Nat.add c b) c) (Nat.add c) (@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c a)) (Nat.add (Nat.add c b)) (@congrArg Nat (Nat → Nat) (Nat.add c a) (Nat.add c b) Nat.add (@congrArg Nat Nat a b (Nat.add c) heq)) c)))) c)) c)) h ``` Since simp uses only single-step `congrArg`/`congrFun` congruence lemmas here, the proof term grows very large, likely quadratic in this case. Can we do better? Every nesting of `congrArg` (and it's little brother `congrFun`) can be turned into a single `congrArg` call. In this PR I make making the smart app builders `Meta.mkCongrArg` and `Meta.mkCongrFun` a bit smarter and not only fuse with `Eq.refl`, but also with `congrArg`/`congrFun`. Now we get, in this simple example, ``` theorem test : ∀ (a b c : Nat), @Eq Nat a b → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c → @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c := fun a b c heq h => @Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c) (@congrArg Nat Prop a b (fun x => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c x) c))) c) c) heq) h ``` Let’s see if it works and how much we gain.
50 lines
1.2 KiB
Text
50 lines
1.2 KiB
Text
x : Nat
|
||
h : f (f x) = x
|
||
⊢ (let y := x * x;
|
||
if True then 1 else y + 1) =
|
||
1
|
||
theorem ex1 : ∀ (x : Nat),
|
||
f (f x) = x →
|
||
(let y := x * x;
|
||
if f (f x) = x then 1 else y + 1) =
|
||
1 :=
|
||
fun x h =>
|
||
Eq.mpr
|
||
(id
|
||
(congrArg (fun x => x = 1)
|
||
(let_congr (Eq.refl (x * x)) fun y =>
|
||
ite_congr (Eq.trans (congrArg (fun x_1 => x_1 = x) h) (eq_self x)) (fun a => Eq.refl 1) fun a =>
|
||
Eq.refl (y + 1))))
|
||
(of_eq_true (eq_self 1))
|
||
x z : Nat
|
||
h : f (f x) = x
|
||
h' : z = x
|
||
⊢ (let y := x;
|
||
y) =
|
||
z
|
||
theorem ex2 : ∀ (x z : Nat),
|
||
f (f x) = x →
|
||
z = x →
|
||
(let y := f (f x);
|
||
y) =
|
||
z :=
|
||
fun x z h h' =>
|
||
Eq.mpr (id (congrArg (fun x => x = z) (let_val_congr (fun y => y) h)))
|
||
(of_eq_true (Eq.trans (congrArg (Eq x) h') (eq_self x)))
|
||
x z : Nat
|
||
⊢ (let α := Nat;
|
||
fun x => 0 + x) =
|
||
id
|
||
p : Prop
|
||
h : p
|
||
⊢ (let n := 10;
|
||
fun x => True) =
|
||
fun z => p
|
||
theorem ex4 : ∀ (p : Prop),
|
||
p →
|
||
(let n := 10;
|
||
fun x => x = x) =
|
||
fun z => p :=
|
||
fun p h =>
|
||
Eq.mpr (id (congrArg (fun x => x = fun z => p) (let_body_congr 10 fun n => funext fun x => eq_self x)))
|
||
(of_eq_true (Eq.trans (congrArg (Eq fun x => True) (funext fun z => eq_true h)) (eq_self fun x => True)))
|