michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(builtin/kernel): reorder congr1 arguments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-09 16:15:44 -08:00
parent fd6f8b1945
commit c45c1748d8
21 changed files with 37 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/builtin/kernel.lean
View file

@ -138,14 +138,17 @@ theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a
theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H1 H2
theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
:= substp (fun h : A → B, f a = h a) (refl (f a)) H
theorem hcongr1 {A : (Type U)} {B : A → (Type U)} {f g : ∀ x, B x} (H : f = g) (a : A) : f a = g a
:= substp (fun h, f a = h a) (refl (f a)) H
theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a
:= hcongr1 H a
theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
:= substp (fun x : A, f a = f x) (refl (f a)) H
theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
:= subst (congr2 f H2) (congr1 b H1)
:= subst (congr2 f H2) (congr1 H1 b)
theorem true_ne_false : ¬ true = false
:= assume H : true = false,
@ -621,7 +624,7 @@ theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
:= calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b }
... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b
... = a ∧ ¬ b : by simp
... = a ∧ ¬ b : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
:= (not_implies a b) ◂ H

4
src/builtin/num.lean
View file

@ -446,7 +446,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A)
calc prim_rec x f zero = prim_rec_fun x f zero (pre zero) : refl _
... = prim_rec_fun x f zero zero : { pre_zero }
... = simp_rec (λ n, x) faux zero zero : refl _
... = x : congr1 zero Heq1,
... = x : congr1 Heq1 zero,
have Hs : ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
from take m,
have Heq1 : pre (succ m) = m,
@ -456,7 +456,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A)
calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _
... = prim_rec_fun x f (succ m) m : congr2 (prim_rec_fun x f (succ m)) Heq1
... = simp_rec (λ n, x) faux (succ m) m : refl _
... = faux (simp_rec (λ n, x) faux m) m : congr1 m Heq2
... = faux (simp_rec (λ n, x) faux m) m : congr1 Heq2 m
... = f (prim_rec x f m) m : refl _,
show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
from and_intro Hz Hs

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

BIN
src/builtin/obj/num.olean
View file

Binary file not shown.

BIN
src/builtin/obj/optional.olean
View file

Binary file not shown.

4
src/builtin/optional.lean
View file

@ -36,14 +36,14 @@ theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
have eq_reps : (λ x, x = a) = (λ x, x = a'),
from abst_inj (inhab A) (some_pred a) (some_pred a') Heq,
show a = a',
from (congr1 a eq_reps) ◂ (refl a)
from (congr1 eq_reps a) ◂ (refl a)
theorem distinct {A : (Type U)} (a : A) : some a ≠ none
:= not_intro (assume N : some a = none,
have eq_reps : (λ x, x = a) = (λ x, false),
from abst_inj (inhab A) (some_pred a) (none_pred A) N,
show false,
from (congr1 a eq_reps) ◂ (refl a))
from (congr1 eq_reps a) ◂ (refl a))
definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
:= ε (inhabited_ex_intro H) (λ x, some x = n)

1
src/kernel/kernel_decls.cpp
View file

@ -41,6 +41,7 @@ MK_CONSTANT(subst_fn, name("subst"));
MK_CONSTANT(substp_fn, name("substp"));
MK_CONSTANT(symm_fn, name("symm"));
MK_CONSTANT(trans_fn, name("trans"));
MK_CONSTANT(hcongr1_fn, name("hcongr1"));
MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr_fn, name("congr"));

3
src/kernel/kernel_decls.h
View file

@ -114,6 +114,9 @@ inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr c
expr mk_trans_fn();
bool is_trans_fn(expr const & e);
inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_hcongr1_fn();
bool is_hcongr1_fn(expr const & e);
inline expr mk_hcongr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hcongr1_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_congr1_fn();
bool is_congr1_fn(expr const & e);
inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }

2
src/library/simplifier/simplifier.cpp
View file

@ -240,7 +240,7 @@ class simplifier_cell::imp {
expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) {
expr const & A = abst_domain(f_type);
expr B = lower_free_vars(abst_body(f_type), 1, 1);
return ::lean::mk_congr1_th(A, B, f, new_f, a, Heq_f);
return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a);
}
expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) {

6
tests/lean/add_assoc.lean.expected.out
View file

@ -9,9 +9,9 @@ Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
Nat::induction_on
a
(eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 c (congr2 Nat::add (Nat::add_zerol b))))
(eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 (congr2 Nat::add (Nat::add_zerol b)) c))
(eq_id (b + c))))
(λ (n : ℕ) (iH : n + (b + c) = n + b + c),
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
(trans (congr1 c (congr2 Nat::add (Nat::add_succl n b))) (Nat::add_succl (n + b) c)))
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 (congr2 Nat::add iH) 1)))
(trans (congr1 (congr2 Nat::add (Nat::add_succl n b)) c) (Nat::add_succl (n + b) c)))
(eq_id (n + b + c + 1))))

2
tests/lean/bad_simp2.lean.expected.out
View file

@ -28,5 +28,5 @@ bad_simp2.lean:51:3: error: failed to create proof for the following proof state
Proof state:
A : Type, B : (Type 1) ⊢ h2 A B = A
theorem T5a (A B : Type) : h2 A B = A :=
eqt_elim (trans (congr1 A (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 A (congr2 eq (Ax1 A))) (eq_id A))))))
eqt_elim (trans (congr1 (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 (congr2 eq (Ax1 A)) A) (eq_id A))))) A)
(eq_id A))

2
tests/lean/find.lean.expected.out
View file

@ -1,7 +1,7 @@
Set: pp::colors
Set: pp::unicode
Imported 'find'
theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a
theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'

2
tests/lean/simp10.lean.expected.out
View file

@ -8,5 +8,5 @@
Proved: one_neq_0
a
fid a
(eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq)
(eqt_elim (trans (trans (congr1 (congr2 neq (gcnst a)) 0) neq_to_not_eq)
(trans (congr2 not (neq_elim one_neq_0)) not_false)))

4
tests/lean/simp17.lean.expected.out
View file

@ -6,8 +6,8 @@
⊥
trans (and_congrr
(λ C::1 : b = 0 ∧ c = 1,
trans (congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1))))
(congr1 1 (congr2 Nat::add (and_eliml C::1))))
trans (congr (congr2 neq (congr1 (congr2 Nat::add (and_elimr C::1)) 0))
(congr1 (congr2 Nat::add (and_eliml C::1)) 1))
(a_neq_a 1))
(λ C::7 : ⊥, refl (b = 0 ∧ c = 1)))
(and_falser (b = 0 ∧ c = 1))

2
tests/lean/simp24.lean.expected.out
View file

@ -9,4 +9,4 @@ funext (λ x : ℕ, trans (imp_congr (refl (x = a)) (λ H : x = a, eq_id x)) (im
λ x : ℕ, ⊤
funext (λ x : ℕ, trans (imp_congr (congr2 (eq x) (Nat::add_zeror a)) (λ H : x = a, eq_id a)) (imp_truer (x = a)))
λ x : ℕ, a = 1 → x > 1
funext (λ x : ℕ, imp_congr (congr1 1 (congr2 eq (Nat::add_zeror a))) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2))
funext (λ x : ℕ, imp_congr (congr1 (congr2 eq (Nat::add_zeror a)) 1) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2))

4
tests/lean/simp26.lean.expected.out
View file

@ -6,12 +6,12 @@
λ x : ℕ, a = 1 → x > f (λ y : ℕ, y + 1)
funext (λ x : ℕ,
imp_congr
(congr1 1 (congr2 eq (Nat::add_zeror a)))
(congr1 (congr2 eq (Nat::add_zeror a)) 1)
(λ C::4 : a = 1, congr2 (Nat::gt x) (congr2 f (funext (λ y : ℕ, congr2 (Nat::add y) C::4)))))
λ x : ℕ, a = 1 → x = 2 → 2 > f (λ y : ℕ, y + 1 + 2)
funext (λ x : ℕ,
imp_congr
(congr1 1 (congr2 eq (Nat::add_zeror a)))
(congr1 (congr2 eq (Nat::add_zeror a)) 1)
(λ C::8 : a = 1,
imp_congr
(refl (x = 2))

2
tests/lean/simp29.lean.expected.out
View file

@ -5,4 +5,4 @@
Assumed: f
Assumed: fNat
(∀ x : ℕ, x > 0) ∧ (∀ x : Bool, f x)
congr1 (∀ x : Bool, f x) (congr2 and (allext (λ x : ℕ, fNat x)))
congr1 (congr2 and (allext (λ x : ℕ, fNat x))) (∀ x : Bool, f x)

8
tests/lean/simp3.lean
View file

@ -40,16 +40,16 @@ print(pr)
*)
theorem congr2_congr1 {A B C : TypeU} {f g : A → B} (h : B → C) (Hfg : f = g) (a : A) :
congr2 h (congr1 a Hfg) = congr2 (λ x, h (x a)) Hfg
:= proof_irrel (congr2 h (congr1 a Hfg)) (congr2 (λ x, h (x a)) Hfg)
congr2 h (congr1 Hfg a) = congr2 (λ x, h (x a)) Hfg
:= proof_irrel (congr2 h (congr1 Hfg a)) (congr2 (λ x, h (x a)) Hfg)
theorem congr2_congr2 {A B C : TypeU} {a b : A} (f : A → B) (h : B → C) (Hab : a = b) :
congr2 h (congr2 f Hab) = congr2 (λ x, h (f x)) Hab
:= proof_irrel (congr2 h (congr2 f Hab)) (congr2 (λ x, h (f x)) Hab)
theorem congr1_congr2 {A B C : TypeU} {a b : A} (f : A → B → C) (Hab : a = b) (c : B):
congr1 c (congr2 f Hab) = congr2 (λ x, f x c) Hab
:= proof_irrel (congr1 c (congr2 f Hab)) (congr2 (λ x, f x c) Hab)
congr1 (congr2 f Hab) c = congr2 (λ x, f x c) Hab
:= proof_irrel (congr1 (congr2 f Hab) c) (congr2 (λ x, f x c) Hab)
rewrite_set proofsimp
add_rewrite congr2_congr1 congr2_congr2 congr1_congr2 : proofsimp

6
tests/lean/simp3.lean.expected.out
View file

@ -20,9 +20,9 @@ trans (Nat::distributel a b (c + d))
Proved: congr1_congr2
⊤
trans (congr (congr2 eq
(congr1 10
(congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))))
(congr1 10 (congr2 Nat::add (if_a_a (a > 0) b))))
(congr1 (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))
10))
(congr1 (congr2 Nat::add (if_a_a (a > 0) b)) 10))
(eq_id (b + 10))
trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x))
(trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))

2
tests/lean/simp31.lean.expected.out
View file

@ -38,5 +38,5 @@ Step: a + (a + b) ===> a + (a + b)
Step: a + (b + a) ===> a + (a + b)
Step: a + (b + 0) + a ===> a + (a + b)
a + (a + b)
trans (trans (congr1 a (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b)))) (Nat::add_assoc a b a))
trans (trans (congr1 (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b))) a) (Nat::add_assoc a b a))
(congr2 (Nat::add a) (Nat::add_comm b a))

2
tests/lean/simp33.lean.expected.out
View file

@ -6,4 +6,4 @@
Assumed: Ax2
Proved: T1
theorem T1 (a : ℕ) : f (f a > 0) :=
eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false)
eqt_elim (trans (trans (congr2 f (congr1 (congr2 Nat::gt (Ax2 a)) 0)) (Ax1 ⊥)) not_false)