fix(tests/lean): adjust tests to reflect changes in the standard library
This commit is contained in:
Leonardo de Moura
parent
ad4c7c20f9
commit
94519b48b1
4 changed files with 27 additions and 75 deletions
|
|
@ -6,16 +6,15 @@
|
|||
-- ====================
|
||||
|
||||
-- Equality.
|
||||
|
||||
import logic.prop
|
||||
|
||||
prelude
|
||||
definition Prop := Type.{0}
|
||||
-- eq
|
||||
-- --
|
||||
|
||||
inductive eq {A : Type} (a : A) : A → Prop :=
|
||||
refl : eq a a
|
||||
|
||||
infix `=` := eq
|
||||
infix `=`:50 := eq
|
||||
definition rfl {A : Type} {a : A} := eq.refl a
|
||||
|
||||
-- proof irrelevance is built in
|
||||
|
|
@ -43,9 +42,9 @@ calc_refl eq.refl
|
|||
calc_trans eq.trans
|
||||
|
||||
namespace eq_ops
|
||||
postfix `⁻¹` := eq.symm
|
||||
reserve infixr `⬝`:75 infixr `⬝` := eq.trans
|
||||
infixr `▸` := eq.subst
|
||||
postfix `⁻¹`:1024 := eq.symm
|
||||
infixr `⬝`:75 := eq.trans
|
||||
infixr `▸`:75 := eq.subst
|
||||
end eq_ops
|
||||
open eq_ops
|
||||
|
||||
|
|
@ -77,7 +76,7 @@ namespace eq
|
|||
(u : P a) :
|
||||
drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u :=
|
||||
(show ∀(H2 : b = c), drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u,
|
||||
from drec_on H2 (take (H2 : b = b), drec_on_id H2 _))
|
||||
from drec_on H2 (fun (H2 : b = b), drec_on_id H2 _))
|
||||
H2
|
||||
end eq
|
||||
|
||||
|
|
@ -127,6 +126,7 @@ theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
|
|||
... = f a₁ b₂ : {H₂})
|
||||
b₂ H₁ H₂
|
||||
|
||||
|
||||
theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
|
||||
(H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
|
||||
f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
|
||||
|
|
@ -143,7 +143,7 @@ theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁
|
|||
congr_arg3_dep f H₁ (drec_on_constant H₁ b₁ ⬝ H₂) H₃
|
||||
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
|
||||
take x, congr_fun H x
|
||||
fun x, congr_fun H x
|
||||
|
||||
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
|
||||
H1 ▸ H2
|
||||
|
|
@ -151,59 +151,11 @@ H1 ▸ H2
|
|||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
|
||||
H1⁻¹ ▸ H2
|
||||
|
||||
theorem eq_true_elim {a : Prop} (H : a = true) : a :=
|
||||
H⁻¹ ▸ trivial
|
||||
|
||||
theorem eq_false_elim {a : Prop} (H : a = false) : ¬a :=
|
||||
assume Ha : a, H ▸ Ha
|
||||
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 Ha)
|
||||
fun Ha, H2 (H1 Ha)
|
||||
|
||||
theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
|
||||
assume Ha, H2 ▸ (H1 Ha)
|
||||
fun Ha, H2 ▸ (H1 Ha)
|
||||
|
||||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 ▸ Ha)
|
||||
|
||||
-- ne
|
||||
-- --
|
||||
|
||||
definition ne {A : Type} (a b : A) := ¬(a = b)
|
||||
infix `≠` := ne
|
||||
|
||||
namespace ne
|
||||
theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b :=
|
||||
H
|
||||
|
||||
theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false :=
|
||||
H1 H2
|
||||
|
||||
theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false :=
|
||||
H rfl
|
||||
|
||||
theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
|
||||
assume H1 : b = a, H (H1⁻¹)
|
||||
end ne
|
||||
|
||||
theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false :=
|
||||
H rfl
|
||||
|
||||
theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c :=
|
||||
H1⁻¹ ▸ H2
|
||||
|
||||
theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c :=
|
||||
H2 ▸ H1
|
||||
|
||||
calc_trans eq_ne_trans
|
||||
calc_trans ne_eq_trans
|
||||
|
||||
theorem p_ne_false {p : Prop} (Hp : p) : p ≠ false :=
|
||||
assume Heq : p = false, Heq ▸ Hp
|
||||
|
||||
theorem p_ne_true {p : Prop} (Hnp : ¬p) : p ≠ true :=
|
||||
assume Heq : p = true, absurd trivial (Heq ▸ Hnp)
|
||||
|
||||
theorem true_ne_false : ¬true = false :=
|
||||
assume H : true = false,
|
||||
H ▸ trivial
|
||||
fun Ha, H2 (H1 ▸ Ha)
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ axiom add_one (n:nat) : n + (succ zero) = succ n
|
|||
axiom add_le_right_inv {n m k : nat} (H : n + k ≤ m + k) : n ≤ m
|
||||
|
||||
theorem succ_le_cancel {n m : nat} (H : succ n ≤ succ m) : n ≤ m
|
||||
:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H)
|
||||
|
||||
end nat
|
||||
end experiment
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
|
|||
:= induction_on n
|
||||
(or.intro_left _ (refl 0))
|
||||
(take m IH, or.intro_right _
|
||||
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
|
||||
(show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹)))
|
||||
|
||||
theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
|
||||
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H)
|
||||
|
|
@ -72,7 +72,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ
|
|||
|
||||
theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m
|
||||
:= calc
|
||||
n = pred (succ n) : pred_succ n⁻¹
|
||||
n = pred (succ n) : (pred_succ n)⁻¹
|
||||
... = pred (succ m) : {H}
|
||||
... = m : pred_succ m
|
||||
|
||||
|
|
@ -473,7 +473,7 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m
|
|||
:= add_one m ▸ add_one n ▸ add_le_right H 1
|
||||
|
||||
theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m
|
||||
:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H)
|
||||
|
||||
theorem self_le_succ (n : ℕ) : n ≤ succ n
|
||||
:= le_intro (add_one n)
|
||||
|
|
@ -757,7 +757,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l
|
|||
:= add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m
|
||||
:= add_le_left_inv (add_succ k n⁻¹ ▸ H)
|
||||
:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H)
|
||||
|
||||
theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m
|
||||
:= add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H)
|
||||
|
|
@ -768,7 +768,7 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m
|
|||
:= add_one m ▸ add_one n ▸ add_lt_right H 1
|
||||
|
||||
theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m
|
||||
:= add_lt_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H)
|
||||
|
||||
theorem lt_self_succ (n : ℕ) : n < succ n
|
||||
:= le_refl (succ n)
|
||||
|
|
@ -1313,9 +1313,9 @@ theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m +
|
|||
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n)
|
||||
:= or.elim (le_total n m)
|
||||
(assume H3 : n ≤ m,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹)))
|
||||
(le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹)))
|
||||
(assume H3 : m ≤ n,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹)))
|
||||
(le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹)))
|
||||
|
||||
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m
|
||||
:= have H2 : k - n + n = m + n, from
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
|
|||
:= induction_on n
|
||||
(or.intro_left _ (eq.refl 0))
|
||||
(take m IH, or.intro_right _
|
||||
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
|
||||
(show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹)))
|
||||
|
||||
theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
|
||||
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H)
|
||||
|
|
@ -66,7 +66,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ
|
|||
|
||||
theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m
|
||||
:= calc
|
||||
n = pred (succ n) : pred_succ n⁻¹
|
||||
n = pred (succ n) : (pred_succ n)⁻¹
|
||||
... = pred (succ m) : {H}
|
||||
... = m : pred_succ m
|
||||
|
||||
|
|
@ -467,7 +467,7 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m
|
|||
:= add_one m ▸ add_one n ▸ add_le_right H 1
|
||||
|
||||
theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m
|
||||
:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H)
|
||||
|
||||
theorem self_le_succ (n : ℕ) : n ≤ succ n
|
||||
:= le_intro (add_one n)
|
||||
|
|
@ -755,7 +755,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l
|
|||
:= add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m
|
||||
:= add_le_left_inv (add_succ k n⁻¹ ▸ H)
|
||||
:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H)
|
||||
|
||||
theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m
|
||||
:= add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H)
|
||||
|
|
@ -766,7 +766,7 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m
|
|||
:= add_one m ▸ add_one n ▸ add_lt_right H 1
|
||||
|
||||
theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m
|
||||
:= add_lt_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H)
|
||||
|
||||
theorem lt_self_succ (n : ℕ) : n < succ n
|
||||
:= le_refl (succ n)
|
||||
|
|
@ -1317,9 +1317,9 @@ theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m +
|
|||
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n)
|
||||
:= or.elim (le_total n m)
|
||||
(assume H3 : n ≤ m,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹)))
|
||||
(le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹)))
|
||||
(assume H3 : m ≤ n,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹)))
|
||||
(le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹)))
|
||||
|
||||
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m
|
||||
:= have H2 : k - n + n = m + n, from
|
||||
|
|
|
|||
Loading…
Reference in a new issue