lean2/tests/lean/hott/len_eq.hlean

import init.ua
open nat unit equiv is_trunc

inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons   : Π {n}, A → vector A n → vector A (succ n)

open vector
notation a :: b := cons a b

definition const {A : Type} : Π (n : nat), A → vector A n
| zero     a := nil
| (succ n) a := a :: const n a

definition head {A : Type} : Π {n : nat}, vector A (succ n) → A
| n (x :: xs) := x

theorem singlenton_vector_unit : ∀ {n : nat} (v w : vector unit n), v = w
| zero     nil        nil        := rfl
| (succ n) (star::xs) (star::ys) :=
  begin
    have h₁ : xs = ys, from singlenton_vector_unit xs ys,
    rewrite h₁
  end

private definition f (n m : nat) (v : vector unit n) : vector unit m := const m star

theorem vn_eqv_vm (n m : nat) : vector unit n ≃ vector unit m :=
equiv.MK (f n m) (f m n)
  (take v : vector unit m, singlenton_vector_unit (f n m (f m n v)) v)
  (take v : vector unit n, singlenton_vector_unit (f m n (f n m v)) v)

theorem vn_eq_vm (n m : nat) : vector unit n = vector unit m :=
ua (vn_eqv_vm n m)

definition vector_inj (A : Type) := ∀ (n m : nat), vector A n = vector A m → n = m

theorem not_vector_inj : ¬ vector_inj unit :=
assume H : vector_inj unit,
have aux₁ : 0 = 1, from H 0 1 (vn_eq_vm 0 1),
lift.down (nat.no_confusion aux₁)

definition cast {A B : Type} (H : A = B) (a : A) : B :=
eq.rec_on H a

open sigma

definition heq {A B : Type} (a : A) (b : B) :=
Σ (H : A = B), cast H a = b

infix `==`:50 := heq

definition heq.type_eq {A B : Type} {a : A} {b : B} : a == b → A = B
| ⟨H, e⟩ := H

definition heq.symm : ∀ {A B : Type} {a : A} {b : B}, a == b → b == a
| A A a a ⟨eq.refl A, eq.refl a⟩ :=  ⟨eq.refl A, eq.refl a⟩

definition heq.trans : ∀ {A B C : Type} {a : A} {b : B} {c : C}, a == b → b == c → a == c
| A A A a a a ⟨eq.refl A, eq.refl a⟩ ⟨eq.refl A, eq.refl a⟩ := ⟨eq.refl A, eq.refl a⟩

theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
| A A (eq.refl A) a := ⟨eq.refl A, eq.refl a⟩

definition default (A : Type) [H : inhabited A] : A :=
inhabited.rec_on H (λ a, a)

definition lem_eq (A : Type) : Type :=
∀ (n m : nat) (v : vector A n) (w : vector A m), v == w → n = m

theorem lem_eq_iff_vector_inj (A : Type) [inh : inhabited A] : lem_eq A ↔ vector_inj A :=
iff.intro
  (assume Hl : lem_eq A,
   assume n m he,
   assert a : A, from default A,
   assert v : vector A n, from const n a,
   have e₁  : v == cast he v, from heq.symm (cast_heq he v),
   Hl n m v (cast he v) e₁)
  (assume Hr : vector_inj A,
   assume n m v w he,
   Hr n m (heq.type_eq he))

theorem lem_eq_of_not_inhabited (A : Type) [ninh : inhabited A → empty] : lem_eq A :=
take (n m : nat),
match n with
| zero      :=
  match m with
  | zero      := take v w He, rfl
  | (succ m₁) :=
    take (v : vector A zero) (w : vector A (succ m₁)),
    empty.elim (ninh (inhabited.mk (head w)))
  end
| (succ n₁) :=
  take (v : vector A (succ n₁)) (w : vector A m),
  empty.elim (ninh (inhabited.mk (head v)))
end