diff --git a/tests/lean/extra/congr.lean b/tests/lean/extra/congr.lean deleted file mode 100644 index d2782de67b..0000000000 --- a/tests/lean/extra/congr.lean +++ /dev/null @@ -1,149 +0,0 @@ -section -variables p : nat → Prop -variables q : nat → nat → Prop -variables f : Π (x y : nat), p x → q x y → nat -example : (0:nat) = 0 := sorry - -#congr @add - -#congr p - -#congr iff - -end - -exit - - -section -variables p : nat → Prop -variables q : Π (n m : nat), p n → p m → Prop -variables r : Π (n m : nat) (H₁ : p n) (H₂ : p m), q n m H₁ H₂ → Prop -variables h : Π (n m : nat) - (H₁ : p n) (H₂ : p m) (H₃ : q n n H₁ H₁) (H₄ : q n m H₁ H₂) - (H₅ : r n m H₁ H₂ H₄) (H₆ : r n n H₁ H₁ H₃), nat - - -definition h_congr (n₁ n₂ : nat) (e₁ : n₁ = n₂) (m₁ m₂ : nat) (e₂ : m₁ = m₂) - (H₁ : p n₁) (H₂ : p m₁) - (H₃ : q n₁ n₁ H₁ H₁) - (H₄ : q n₁ m₁ H₁ H₂) - (H₅ : r n₁ m₁ H₁ H₂ H₄) - (H₆ : r n₁ n₁ H₁ H₁ H₃) : - h n₁ m₁ H₁ H₂ H₃ H₄ H₅ H₆ = - h n₂ m₂ (eq.drec_on e₁ H₁) - (eq.drec_on e₂ H₂) - (eq.drec_on e₁ H₃) - (eq.drec_on e₁ (eq.drec_on e₂ H₄)) - (eq.drec_on e₁ (eq.drec_on e₂ H₅)) - (eq.drec_on e₁ H₆) := -begin - apply eq.drec_on e₁, - apply eq.drec_on e₂, - apply rfl -end - --- set_option pp.implicit true --- print h_congr -#congr h - -exit - -eq.drec_on e₁ (eq.drec_on e₂ (eq.refl (h n₂ m₂ (eq.rec_on e₁ H₁) (eq.rec_on e₂ H₂) (eq.drec_on e₁ H₃) - (eq.drec_on e₁ (eq.drec_on e₂ H₄)) - (eq.drec_on e₁ (eq.drec_on e₂ H₅)) - (eq.drec_on e₁ H₆)))) - -sorry - -exit - - - -q x₁ H₁) : - h x₁ H₁ H₂ = h x₂ (eq.rec_on e H₁) (eq.drec_on e H₂) := -eq.drec_on e (eq.refl (h x₁ (eq.rec_on (eq.refl x₁) H₁) (eq.drec_on (eq.refl x₁) H₂))) - -exit - -variables h₂ : Π (n : nat) (H₁ : p n) (H₂ : q n H₁) (H₃ : r n H₁ H₂), nat - -definition h_congr (x₁ x₂ : nat) (e : x₁ = x₂) (H₁ : p x₁) (H₂ : q x₁ H₁) : - h x₁ H₁ H₂ = h x₂ (eq.rec_on e H₁) (eq.drec_on e H₂) := -eq.drec_on e (eq.refl (h x₁ (eq.rec_on (eq.refl x₁) H₁) (eq.drec_on (eq.refl x₁) H₂))) - -definition h_congr₂ (x₁ x₂ : nat) (e : x₁ = x₂) (H₁ : p x₁) (H₂ : q x₁ H₁) (H₃ : r x₁ H₁ H₂) : - h₂ x₁ H₁ H₂ H₃ = h₂ x₂ (eq.rec_on e H₁) (eq.drec_on e H₂) (eq.drec_on e H₃) := -eq.drec_on e (eq.refl (h₂ x₁ (eq.rec_on (eq.refl x₁) H₁) (eq.drec_on (eq.refl x₁) H₂) (eq.drec_on (eq.refl x₁) H₃))) - - -definition h_congr₃ (x₁ x₂ : nat) (e : x₁ = x₂) (H₁ : p x₁) (H₂ : q x₁ H₁) (H₃ : r x₁ H₁ H₂) : - h₂ x₁ H₁ H₂ H₃ = h₂ x₂ (eq.rec_on e H₁) (eq.drec_on e H₂) (eq.drec_on e H₃) := -begin - congruence, - apply e -end - - --- print h_congr₃ - --- exit - -set_option pp.all true -print h_congr₂ - - -#congr h - -exit - -set_option pp.all true -print h_congr - -#congr h -end - - - - -exit -variables g : Π (A : Type) (x y : A) (B : Type) (z : B), x = y → y == z → nat - -#congr g - - -exit - - - -lemma f_congr - (x₁ x₂ : nat) (e₁ : x₁ = x₂) - (y₁ y₂ : nat) (e₂ : y₁ = y₂) - (H₁ : p x₁) - (H₂ : q x₁ y₁) : - f x₁ y₁ H₁ H₂ = - f x₂ y₂ (@eq.rec_on nat x₁ (λ (a : ℕ), p a) x₂ e₁ H₁) - (@eq.rec_on nat x₁ (λ (a : ℕ), q a y₂) x₂ e₁ (@eq.rec_on nat y₁ (λ (a : ℕ), q x₁ a) y₂ e₂ H₂)) := -let R := (eq.refl (f x₁ y₁ (@eq.rec_on nat x₁ (λ (a : ℕ), p a) x₁ (eq.refl x₁) H₁) (@eq.rec_on nat x₁ (λ (a : ℕ), q a y₁) x₁ (eq.refl x₁) (@eq.rec_on nat y₁ (λ (a : ℕ), q x₁ a) y₁ (eq.refl y₁) H₂)))) in -@eq.drec_on nat x₁ - (λ (z : ℕ) (H : x₁ = z), - f x₁ y₁ H₁ H₂ = - f z y₂ (@eq.rec_on nat x₁ (λ a, p a) z H H₁) - (@eq.rec_on nat x₁ (λ a, q a y₂) z H (@eq.rec_on nat y₁ (λ a, q x₁ a) y₂ e₂ H₂))) - x₂ e₁ - (@eq.drec_on nat y₁ - (λ (z : ℕ) (H : y₁ = z), - f x₁ y₁ H₁ H₂ = - f x₁ z (@eq.rec_on nat x₁ (λ a, p a) x₁ (eq.refl x₁) H₁) - (@eq.rec_on nat x₁ (λ a, q a z) x₁ (eq.refl x₁) (@eq.rec_on nat y₁ (λ a, q x₁ a) z H H₂))) - y₂ e₂ R) - - - -/- - - f x₁ y₁ H₁ H₂ = - f x₁ y₂ (@eq.rec_on nat x₁ (λ a, p a) x₁ (eq.refl x₁) H₁) - (@eq.rec_on nat x₁ (λ a, q a y₂) x₁ (eq.refl x₁) (@eq.rec_on nat y₁ (λ a, q x₁ a) y₂ e₂ H₂))) - --/ diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean deleted file mode 100644 index 00b860dff8..0000000000 --- a/tests/lean/run/sum_bug.lean +++ /dev/null @@ -1,64 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura, Jeremy Avigad -open inhabited decidable -namespace play --- TODO: take this outside the namespace when the inductive package handles it better -inductive sum (A B : Type) : Type -| inl : A → sum -| inr : B → sum - -namespace sum -reserve infixr `+`:25 -infixr `+` := sum - -open eq - -theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := -let f := λs, sum.rec_on s (λa, a1 = a) (λb, false) in -have H1 : f (inl B a1), from rfl, -have H2 : f (inl B a2), from subst H H1, -H2 - -theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false := -let f := λs, sum.rec_on s (λa', a = a') (λb, false) in -have H1 : f (inl B a), from rfl, -have H2 : f (inr A b), from subst H H1, -H2 - -theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 := -let f := λs, sum.rec_on s (λa, false) (λb, b1 = b) in -have H1 : f (inr A b1), from rfl, -have H2 : f (inr A b2), from subst H H1, -H2 - -attribute [instance] -theorem sum_inhabited_left {A B : Type} (H : inhabited A) : inhabited (A + B) := -inhabited.mk (inl B (default A)) - -attribute [instance] -theorem sum_inhabited_right {A B : Type} (H : inhabited B) : inhabited (A + B) := -inhabited.mk (inr A (default B)) - -attribute [instance] -theorem sum_eq_decidable {A B : Type} (s1 s2 : A + B) - (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) - (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := -sum.rec_on s1 - (take a1, show decidable (inl B a1 = s2), from - sum.rec_on s2 - (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) - (take b2, - have H3 : (inl B a1 = inr A b2) ↔ false, - from iff.intro inl_neq_inr (assume H4, false.elim H4), - show decidable (inl B a1 = inr A b2), from decidable_of_decidable_of_iff _ (iff.symm H3))) - (take b1, show decidable (inr A b1 = s2), from - sum.rec_on s2 - (take a2, - have H3 : (inr A b1 = inl B a2) ↔ false, - from iff.intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false.elim H4), - show decidable (inr A b1 = inl B a2), from decidable_of_decidable_of_iff _ (iff.symm H3)) - (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) - -end sum -end play diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean deleted file mode 100644 index 6f1526da43..0000000000 --- a/tests/lean/run/uuu.lean +++ /dev/null @@ -1,153 +0,0 @@ -prelude --- Porting Vladimir's file to Lean -notation `assume` binders `,` r:(scoped f, f) := r -notation `take` binders `,` r:(scoped f, f) := r - -inductive empty : Type -inductive unit : Type -| tt : unit -definition tt := @unit.tt -inductive nat : Type -| O : nat -| S : nat → nat - -inductive paths {A : Type} (a : A) : A → Type -| idpath : paths a -definition idpath := @paths.idpath - -inductive sum (A : Type) (B : Type) : Type -| inl : A -> sum -| inr : B -> sum - -definition coprod := sum -definition ii1fun {A : Type} (B : Type) (a : A) := sum.inl B a -definition ii2fun (A : Type) {B : Type} (b : B) := sum.inr A b -definition ii1 {A : Type} {B : Type} (a : A) := sum.inl B a -definition ii2 {A : Type} {B : Type} (b : B) := sum.inl A b - -inductive total2 {T: Type} (P: T → Type) : Type -| tpair : Π (t : T) (tp : P t), total2 -definition tpair := @total2.tpair - -definition pr1 {T : Type} {P : T → Type} (tp : total2 P) : T -:= total2.rec (λ a b, a) tp -definition pr2 {T : Type} {P : T → Type} (tp : total2 P) : P (pr1 tp) -:= total2.rec (λ a b, b) tp - -inductive Phant (T : Type) : Type -| phant : Phant - -definition fromempty {X : Type} : empty → X -:= λe, empty.rec (λe, X) e - -definition tounit {X : Type} : X → unit -:= λx, tt - -definition termfun {X : Type} (x : X) : unit → X -:= λt, x - -definition idfun (T : Type) := λt : T, t - -definition funcomp {X : Type} {Y : Type} {Z : Type} (f : X → Y) (g : Y → Z) -:= λx, g (f x) - -infixl `∘`:60 := funcomp - -definition iteration {T : Type} (f : T → T) (n : nat) : T → T -:= nat.rec (idfun T) (λ m fm, funcomp fm f) n - -definition adjev {X : Type} {Y : Type} (x : X) (f : X → Y) := f x - -definition adjev2 {X : Type} {Y : Type} (phi : ((X → Y) → Y ) → Y ) : X → Y -:= λx, phi (λf, f x) - -definition dirprod (X : Type) (Y : Type) := total2 (λ x : X, Y) -definition dirprodpair {X : Type} {Y : Type} := @tpair _ (λ x : X, Y) -definition dirprodadj {X : Type} {Y : Type} {Z : Type} (f : dirprod X Y → Z ) : X → Y → Z -:= λx y, f (dirprodpair x y) -definition dirprodf {X : Type} {Y : Type} {X' : Type} {Y' : Type} (f : X → Y) (f' : X' → Y') (xx' : dirprod X X') : dirprod Y Y' -:= dirprodpair (f (pr1 xx')) (f' (pr2 xx')) -definition ddualand {X : Type} {Y : Type} {P : Type} (xp : (X → P) → P) (yp : (Y → P) → P) : (dirprod X Y → P) → P -:= λ X0, - let int1 := λ (ypp : (Y → P) → P) (x : X), yp (λ y : Y, X0 (dirprodpair x y)) in - xp (int1 yp) - -definition neg (X : Type) : Type := X → empty -definition negf {X : Type} {Y : Type} (f : X → Y) : neg Y → neg X -:= λ (phi : Y → empty) (x : X), phi (f x) - -definition dneg (X : Type) : Type := (X → empty) → empty -definition dnegf {X : Type} {Y : Type} (f : X → Y) : dneg X → dneg Y -:= negf (negf f) - -definition todneg (X : Type) : X → dneg X -:= adjev - -definition dnegnegtoneg {X : Type} : dneg (neg X) → neg X -:= adjev2 - -lemma dneganddnegl1 {X : Type} {Y : Type} (dnx : dneg X) (dny : dneg Y) : neg (X → neg Y) -:= take X2 : X → neg Y, - have X3 : dneg X → neg Y, from - take xx : dneg X, dnegnegtoneg (dnegf X2 xx), - dny (X3 dnx) - -definition logeq (X : Type) (Y : Type) := dirprod (X → Y) (Y → X) -infix `<->`:25 := logeq -infix `↔`:25 := logeq - -definition logeqnegs {X : Type} {Y : Type} (l : X ↔ Y) : (neg X) ↔ (neg Y) -:= dirprodpair (negf (pr2 l)) (negf (pr1 l)) - -infix `=`:50 := paths - -definition pathscomp0 {X : Type} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c -:= paths.rec e1 e2 - -definition pathscomp0rid {X : Type} {a b : X} (e1 : a = b) : pathscomp0 e1 (idpath b) = e1 -:= idpath _ - -definition pathsinv0 {X : Type} {a b : X} (e : a = b) : b = a -:= paths.rec (idpath _) e - -definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P a) : P b -:= paths.rec H2 H1 - -infixr `▸`:75 := transport -infixr `⬝`:75 := pathscomp0 -postfix `⁻¹`:100 := pathsinv0 - -definition idinv {X : Type} (x : X) : (idpath x)⁻¹ = idpath x -:= idpath (idpath x) - -definition idtrans {A : Type} (x : A) : (idpath x) ⬝ (idpath x) = (idpath x) -:= idpath (idpath x) - -definition pathsinv0l {X : Type} {a b : X} (e : a = b) : e⁻¹ ⬝ e = idpath b -:= paths.rec (idinv a⁻¹ ▸ idtrans a) e - -definition pathsinv0r {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = idpath y -:= paths.rec (idinv x⁻¹ ▸ idtrans x) p - -definition pathsinv0inv0 {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p -:= paths.rec (idpath (idpath x)) p - -definition pathsdirprod {X : Type} {Y : Type} {x1 x2 : X} {y1 y2 : Y} (ex : x1 = x2) (ey : y1 = y2 ) : dirprodpair x1 y1 = dirprodpair x2 y2 -:= ex ▸ ey ▸ idpath (dirprodpair x1 y1) - -definition maponpaths {T1 : Type} {T2 : Type} (f : T1 → T2) {t1 t2 : T1} (e : t1 = t2) : f t1 = f t2 -:= e ▸ idpath (f t1) - -definition ap {T1 : Type} {T2 : Type} := @maponpaths T1 T2 - -definition maponpathscomp0 {X : Type} {Y : Type} {x y z : X} (f : X → Y) (p : x = y) (q : y = z) : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) -:= paths.rec (idpath _) q - -definition maponpathsinv0 {X : Type} {Y : Type} (f : X → Y) {x1 x2 : X} (e : x1 = x2 ) : ap f (e⁻¹) = (ap f e)⁻¹ -:= paths.rec (idpath _) e - -lemma maponpathsidfun {X : Type} {x x' : X} (e : x = x') : ap (idfun X) e = e -:= paths.rec (idpath _) e - -lemma maponpathscomp {X : Type} {Y : Type} {Z : Type} {x x' : X} (f : X → Y) (g : Y → Z) (e : x = x') : ap g (ap f e) = ap (f ∘ g) e -:= paths.rec (idpath _) e