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

fix(frontends/lean/pp): make sure pp and parser are using the same precedences

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-19 12:46:14 -08:00
parent 02bd166793
commit bff5a6bfb2
35 changed files with 94 additions and 101 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/notation.h
View file

@ -5,9 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <limits>
namespace lean {
constexpr unsigned g_eq_precedence = 50;
constexpr unsigned g_arrow_precedence = 25;
constexpr unsigned g_app_precedence = std::numeric_limits<unsigned>::max();
class environment;
class io_state;
void init_builtin_notation(environment const & env, io_state & st);

11
src/frontends/lean/parser.cpp
View file

@ -123,9 +123,6 @@ static unsigned g_level_plus_prec = 10;
static unsigned g_level_cup_prec = 5;
// ==========================================
// precedence (aka binding power) for function application
constexpr unsigned app_lbp = std::numeric_limits<unsigned>::max();
// A name that can't be created by the user.
// It is used as placeholder for parsing A -> B expressions which
// are syntax sugar for (Pi (_ : A), B)
@ -825,7 +822,7 @@ class parser::imp {
if (imp_args[i]) {
args.push_back(save(mk_placeholder(), pos()));
} else {
args.push_back(parse_expr(app_lbp));
args.push_back(parse_expr(g_app_precedence));
}
}
return mk_app(args);
@ -1312,20 +1309,20 @@ class parser::imp {
name const & id = curr_name();
auto it = m_local_decls.find(id);
if (it != m_local_decls.end()) {
return app_lbp;
return g_app_precedence;
} else {
optional<unsigned> prec = get_lbp(m_env, id);
if (prec)
return *prec;
else
return app_lbp;
return g_app_precedence;
}
}
case scanner::token::Eq : return g_eq_precedence;
case scanner::token::Arrow : return g_arrow_precedence;
case scanner::token::LeftParen: case scanner::token::NatVal: case scanner::token::DecimalVal:
case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder:
return app_lbp;
return g_app_precedence;
default:
return 0;
}

4
src/frontends/lean/pp.cpp
View file

@ -431,8 +431,10 @@ class pp_fn {
return g_eq_precedence;
} else if (is_arrow(e)) {
return g_arrow_precedence;
} else {
} else if (is_lambda(e) || is_pi(e) || is_let(e)) {
return 0;
} else {
return g_app_precedence;
}
}

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

@ -7,4 +7,4 @@
Assumed: b
Assumed: Ax2
Proved: T2
Theorem T2 (a : ℤ) : (P a a) ⇒ (f a a) := Discharge (λ H : P a a, Ax1 a a H)
Theorem T2 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H)

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

@ -12,8 +12,8 @@
n + m
n + x + m
Set: lean::pp::coercion
(nat_to_int n) + x + (nat_to_int m) + (nat_to_int 10)
x + (nat_to_int n) + (nat_to_int m) + (nat_to_int 10)
(nat_to_int (n + m + 10)) + x
nat_to_int n + x + nat_to_int m + nat_to_int 10
x + nat_to_int n + nat_to_int m + nat_to_int 10
nat_to_int (n + m + 10) + x
Set: lean::pp::notation
Int::add (nat_to_int (Nat::add (Nat::add n m) 10)) x

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

@ -8,9 +8,9 @@
Assumed: n
x + i + 1 + n
Set: lean::pp::coercion
x + (int_to_real i) + (nat_to_real 1) + (nat_to_real n)
x * (int_to_real i) + x
x - (int_to_real i) + x - x ≥ (nat_to_real 0)
x + int_to_real i + nat_to_real 1 + nat_to_real n
x * int_to_real i + x
x - int_to_real i + x - x ≥ nat_to_real 0
x < x
x ≤ x
x > x

8
tests/lean/arith4.lean.expected.out
View file

@ -3,7 +3,7 @@
Assumed: x
sin x
sin (x + -1 * (π / 2))
(sin x) / (sin (x + -1 * (π / 2)))
(sin (x + -1 * (π / 2))) / (sin x)
1 / (sin (x + -1 * (π / 2)))
1 / (sin x)
sin x / sin (x + -1 * (π / 2))
sin (x + -1 * (π / 2)) / sin x
1 / sin (x + -1 * (π / 2))
1 / sin x

12
tests/lean/arith5.lean.expected.out
View file

@ -1,9 +1,9 @@
Set: pp::colors
Set: pp::unicode
Assumed: x
(1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x)))
(1 + (exp (-2 * x))) / (2 * (exp (-1 * x)))
(1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x))) / ((1 + (exp (-2 * x))) / (2 * (exp (-1 * x))))
(1 + (exp (-2 * x))) / (2 * (exp (-1 * x))) / ((1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x))))
1 / ((1 + (exp (-2 * x))) / (2 * (exp (-1 * x))))
1 / ((1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x))))
(1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x))
(1 + exp (-2 * x)) / (2 * exp (-1 * x))
(1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)) / ((1 + exp (-2 * x)) / (2 * exp (-1 * x)))
(1 + exp (-2 * x)) / (2 * exp (-1 * x)) / ((1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)))
1 / ((1 + exp (-2 * x)) / (2 * exp (-1 * x)))
1 / ((1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)))

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

@ -6,5 +6,5 @@
Assumed: H1
Assumed: H2
Proved: T1
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := SubstP (λ x : ℤ, (g x) > 0) H2 H1
Axiom H2 : g a > 0
Theorem T1 : g b > 0 := SubstP (λ x : ℤ, g x > 0) H2 H1

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

@ -9,7 +9,7 @@
Error (line: 12, pos: 6) type mismatch at application
f m v1
Function type:
Π (n : ℕ), (vector ℤ n) → ℤ
Π (n : ℕ), vector ℤ n → ℤ
Arguments types:
m : ℕ
v1 : vector ℤ (m + 0)

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

@ -28,5 +28,5 @@ h (h r s) r : S
g (g (t2r a) b) (t2r a)
h (h r s) r
Set: lean::pp::notation
(t2r a) ++ b ++ (t2r a)
t2r a ++ b ++ t2r a
r ++ s ++ r

8
tests/lean/conv.lean.expected.out
View file

@ -2,7 +2,7 @@
Set: pp::unicode
Defined: id
Assumed: p
λ x : id ℤ, x : (id ℤ) → (id ℤ)
λ x : id ℤ, x : id ℤ → id ℤ
Assumed: f
p f : Bool
Defined: c
@ -11,9 +11,9 @@ p f : Bool
g a : Bool
Defined: c2
Assumed: b
c2::explicit : Π (T : Type), (Type 3) → T → (Type 3)
c2::explicit : Π (T : Type), Type 3 → T → Type 3
Assumed: g2
g2 : (c2 (Type 2) b) → Bool
g2 : c2 (Type 2) b → Bool
Assumed: a2
g2 a2 : Bool
λ x : c2 (Type 1) b, g2 x : (c2 (Type 1) b) → Bool
λ x : c2 (Type 1) b, g2 x : c2 (Type 1) b → Bool

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

@ -22,7 +22,7 @@ Definition R::explicit (A A' : Type)
(B : A → Type)
(B' : A' → Type)
(H : (Π x : A, B x) = (Π x : A', B' x))
(a : A) : (B a) = (B' (C (D H) a)) :=
(a : A) : B a = B' (C (D H) a) :=
R H a
Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

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

@ -22,7 +22,7 @@ Definition R::explicit (A A' : Type)
(B : A → Type)
(B' : A' → Type)
(H : (Π x : A, B x) = (Π x : A', B' x))
(a : A) : (B a) = (B' (C (D H) a)) :=
(a : A) : B a = B' (C (D H) a) :=
R H a
Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

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

@ -8,7 +8,7 @@
Assumed: F2
Assumed: H
Assumed: a
Eta (F2 a) : (λ x : B, F2 a x) == (F2 a)
Eta (F2 a) : (λ x : B, F2 a x) == F2 a
Abst (λ a : A, Trans (Symm (Eta (F1 a))) (Trans (Abst (λ b : B, H a b)) (Eta (F2 a)))) :
(λ x : A, F1 x) == (λ x : A, F2 x)
Abst (λ a : A, Abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)

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

@ -3,4 +3,4 @@
Assumed: i
i = 0 : Bool
Set: lean::pp::coercion
i = (nat_to_int 0) : Bool
i = nat_to_int 0 : Bool

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

@ -6,5 +6,5 @@
Assumed: H1
Assumed: H2
Proved: T1
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := Subst H2 H1
Axiom H2 : g a > 0
Theorem T1 : g b > 0 := Subst H2 H1

10
tests/lean/implicit1.lean.expected.out
View file

@ -1,13 +1,13 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
∀ a : ℤ, (f a a) > 0
∀ a b : ℤ, (f a b) > 0
∀ a : ℤ, f a a > 0
∀ a b : ℤ, f a b > 0
Assumed: g
∀ (a : ℤ) (b : ℝ), (g a b) > 0
∀ a b : ℤ, (g a (f a b)) > 0
∀ (a : ℤ) (b : ℝ), g a b > 0
∀ a b : ℤ, g a (f a b) > 0
Set: lean::pp::coercion
∀ a b : ℤ, (g a (int_to_real (f a b))) > (nat_to_int 0)
∀ a b : ℤ, g a (int_to_real (f a b)) > nat_to_int 0
λ a : ℕ, a + 1
λ a b : ℕ, a + b
λ a b c : ℤ, a + c + b

2
tests/lean/interactive/t7.lean.expected.out
View file

@ -5,7 +5,7 @@
# Assumed: Ax
# Assumed: a
# Proof state:
x : ℤ ⊢ (q a x) ⇒ (p x)
x : ℤ ⊢ q a x ⇒ p x
## Proof state:
H : q a x, x : ℤ ⊢ p x
## Proof state:

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

@ -11,4 +11,4 @@ let a : ℕ := 10 in a + 1 : ℕ
30
let a : ℤ := 20 in a + 10 : ℤ
Set: lean::pp::coercion
let a : ℤ := nat_to_int 20 in a + (nat_to_int 10)
let a : ℤ := nat_to_int 20 in a + nat_to_int 10

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

@ -8,7 +8,7 @@
λ (f : N → N) (y : N), g (f a)
λ (a : N) (f : N → N) (g : (N → N) → N → N) (h : N → N → N) (z : N), h (g (λ x : N, f (f x)) (f a)) (f a)
λ (a b : N) (g : Bool → N) (y : Bool), g (a == b)
λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : Type U), g (Π x : a, b x)
λ (a : Type) (b : a → Type) (g : Type U → Bool) (y : Type U), g (Π x : a, b x)
λ (f : N → N) (y z : N), g (f a)
λ (f g : N → N) (y z : N), g (f a)
λ (f : N → N) (y z : N), P (f a) y z

24
tests/lean/scope.lean.expected.out
View file

@ -11,22 +11,16 @@
Proved: f_eq_g
Proved: Inj
Definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
Theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, (f x y) = (f y x)) : f = (g A f) :=
Theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, f x y = f y x) : f = g A f :=
Abst (λ x : A,
Abst (λ y : A,
let L1 : (f x y) = (f y x) := H1 x y,
L2 : (f y x) = (g A f x y) := Refl (g A f x y)
in Trans L1 L2))
Theorem Inj (A B : Type)
(h : A → B)
(hinv : B → A)
(Inv : Π x : A, (hinv (h x)) = x)
(x y : A)
(H : (h x) = (h y)) : x = y :=
let L1 : (hinv (h x)) = (hinv (h y)) := Congr2 hinv H,
L2 : (hinv (h x)) = x := Inv x,
L3 : (hinv (h y)) = y := Inv y,
L4 : x = (hinv (h x)) := Symm L2,
L5 : x = (hinv (h y)) := Trans L4 L1
let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := Refl (g A f x y) in Trans L1 L2))
Theorem Inj (A B : Type) (h : A → B) (hinv : B → A) (Inv : Π x : A, hinv (h x) = x) (x y : A) (H : h x = h y) : x =
y :=
let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H,
L2 : hinv (h x) = x := Inv x,
L3 : hinv (h y) = y := Inv y,
L4 : x = hinv (h x) := Symm L2,
L5 : x = hinv (h y) := Trans L4 L1
in Trans L5 L3
10

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

@ -5,6 +5,6 @@
Proved: T1
Defined: h
Proved: T2
Theorem T2 (a b : Bool) : (h a b) ⇒ (f b) ⇒ a :=
Theorem T2 (a b : Bool) : h a b ⇒ f b ⇒ a :=
Discharge
(λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))

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

@ -3,7 +3,7 @@
Assumed: f
Proved: T1
Proved: T2
Theorem T1 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a) :=
Theorem T1 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : f (f a a) b = f (f b c) a :=
Congr (Congr (Refl f) (Congr (Congr (Refl f) H1) H2)) (Symm H1)
Theorem T2 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)) :=
Theorem T2 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : f (f a c) = f (f b a) :=
Congr (Refl f) (Congr (Congr (Refl f) H1) (Symm H2))

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

@ -1,5 +1,5 @@
Set: pp::colors
Set: pp::unicode
Proved: T1
Theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : (f (f a)) = (f (f b)) :=
Theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : f (f a) = f (f b) :=
Congr (Refl f) (Congr (Refl f) assumption)

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

@ -2,5 +2,5 @@
Set: pp::unicode
Defined: f
Proved: T
Theorem T (a b : Bool) : a ∨ b ⇒ (f b) ⇒ a :=
Theorem T (a b : Bool) : a ∨ b ⇒ f b ⇒ a :=
Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))

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

@ -33,7 +33,7 @@ update (const three ⊥) two ⊤ : vector Bool three
select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
map type --->
map::explicit : Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
map::explicit : Π (A B C : Type) (n : N), (A → B → C) → vector A n → vector B n → vector C n
map normal form -->
λ (A B C : Type)

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

@ -6,7 +6,7 @@
⊤
Assumed: a
a ⊕ a ⊕ a
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → a == b → (P b)
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b
Proved: EM2
EM2 : Π a : Bool, a ∨ ¬ a
EM2 a : a ∨ ¬ a

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

@ -5,5 +5,5 @@ let x := ⊤,
y := ⊤,
z := x ∧ y,
f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2
in (f x y) ∨ z
in f x y ∨ z
⊤

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

@ -1,4 +1,4 @@
Set: pp::colors
Set: pp::unicode
λ x x : Bool, x
let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z
let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in f x y ∨ z

12
tests/lean/tst15.lean.expected.out
View file

@ -3,7 +3,7 @@
Assumed: x
x : Type U+3 ⊔ M+2 ⊔ 3
Assumed: f
f : (Type U+10) → Type
f : Type U+10 → Type
f x : Type
Type 4 : Type 5
x : Type U+3 ⊔ M+2 ⊔ 3
@ -14,9 +14,9 @@ Type U ⊔ M : Type U+1 ⊔ M+1
Type U ⊔ M ⊔ 3 : Type U+1 ⊔ M+1 ⊔ 4
Type U+1 ⊔ M ⊔ 3
Type U+1 ⊔ M ⊔ 3 : Type U+2 ⊔ M+1 ⊔ 4
(Type U) → (Type 5)
(Type U) → (Type 5) : Type U+1 ⊔ 6
(Type M ⊔ 3) → (Type U+5) : Type M+1 ⊔ 4 ⊔ U+6
(Type M ⊔ 3) → (Type U) → (Type 5)
(Type M ⊔ 3) → (Type U) → (Type 5) : Type M+1 ⊔ 6 ⊔ U+1
Type U → Type 5
Type U → Type 5 : Type U+1 ⊔ 6
Type M ⊔ 3 → Type U+5 : Type M+1 ⊔ 4 ⊔ U+6
Type M ⊔ 3 → Type U → Type 5
Type M ⊔ 3 → Type U → Type 5 : Type M+1 ⊔ 6 ⊔ U+1
Type U

24
tests/lean/tst16.lean.expected.out
View file

@ -1,17 +1,17 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
∀ a b : Type, (f a) = (f b)
∀ a b : Type, f a = f b
Assumed: g
∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
∃ (a b : Type) (c : Bool), g c ((f a) = (f b))
∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a)
∀ (a b : Type) (c : Bool), g c ((f a) = (f b)) : Bool
∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
∀ a b : Type, (f a) = (f b)
∃ a b : Type, (f a) = (f b) ∧ (f a)
∃ a b : Type, (f a) = (f b) ∨ (f b)
∀ (a b : Type) (c : Bool), g c (f a = f b)
∃ (a b : Type) (c : Bool), g c (f a = f b)
∀ (a b : Type) (c : Bool), g c (f a) = f b ⇒ f a
∀ (a b : Type) (c : Bool), g c (f a = f b) : Bool
∀ (a b : Type) (c : Bool), g c (f a = f b)
∀ a b : Type, f a = f b
∃ a b : Type, f a = f b ∧ f a
∃ a b : Type, f a = f b ∨ f b
Assumed: a
(f a) ∨ (f a)
(f a) = a ∨ (f a)
(f a) = a ∧ (f a)
f a ∨ f a
f a = a ∨ f a
f a = a ∧ f a

7
tests/lean/tst17.lean.expected.out
View file

@ -2,9 +2,8 @@
Set: pp::unicode
Assumed: f
Assumed: g
∀ a b : Type, ∃ c : Type, (g a b) = (f c)
∀ a b : Type, ∃ c : Type, (g a b) = (f c) : Bool
∀ a b : Type, ∃ c : Type, g a b = f c
∀ a b : Type, ∃ c : Type, g a b = f c : Bool
(λ a : Type,
(λ b : Type, if ((λ x : Type, if ((g a b) == (f x)) ⊥ ⊤) == (λ x : Type, ⊤)) ⊥ ⊤) ==
(λ x : Type, ⊤)) ==
(λ b : Type, if ((λ x : Type, if (g a b == f x) ⊥ ⊤) == (λ x : Type, ⊤)) ⊥ ⊤) == (λ x : Type, ⊤)) ==
(λ x : Type, ⊤)

3
tests/lean/tst4.lean.expected.out
View file

@ -10,8 +10,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
Assumed: EqNice
EqNice::explicit N n1 n2
f::explicit N n1 n2 : N
Congr::explicit :
Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → (f a) == (g b)
Congr::explicit : Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
f::explicit N n1 n2
Assumed: a
Assumed: b

12
tests/lean/tst6.lean.expected.out
View file

@ -17,10 +17,10 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit
b2
(Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := CongrH H1 H2
Set: lean::pp::implicit
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := Congr (Congr (Refl h) H1) H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := CongrH H1 H2
Proved: Example1
Set: lean::pp::implicit
Theorem Example1 (a b c d : N)
@ -31,7 +31,7 @@ Theorem Example1 (a b c d : N)
DisjCases::explicit
(eq::explicit N a b ∧ eq::explicit N b c)
(eq::explicit N a d ∧ eq::explicit N d c)
((h a b) == (h c b))
(h a b == h c b)
H
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
CongrH::explicit
@ -103,14 +103,14 @@ Theorem Example2 (a b c d : N)
(Refl::explicit N b))
Proved: Example3
Set: lean::pp::implicit
Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b :=
DisjCases
H
(λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
(λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
Proved: Example4
Set: lean::pp::implicit
Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a c = h c a :=
DisjCases
H
(λ H1 : a = b ∧ b = e ∧ b = c,