From 5daff18017b129d1e887faeb604ea1a90ba27cb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Nov 2014 18:30:11 -0800 Subject: [PATCH] test(tests/lean/run): pre-quotient experiment --- tests/lean/run/pquot.lean | 99 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 tests/lean/run/pquot.lean diff --git a/tests/lean/run/pquot.lean b/tests/lean/run/pquot.lean new file mode 100644 index 000000000..1ec4a19ff --- /dev/null +++ b/tests/lean/run/pquot.lean @@ -0,0 +1,99 @@ +import logic.cast data.list data.sigma + +-- The (pre-)quotient type kernel extension would add the following constants +-- quot, pquot.mk, pquot.eqv and pquot.rec +-- and a computational rule, which we call pquot.comp here. +-- Note that, these constants do not assume the environment contains = +constant pquot.{l} {A : Type.{l}} (R : A → A → Prop) : Type.{l} + +constant pquot.abs {A : Type} (R : A → A → Prop) : A → pquot R +-- pquot.eqv is a way to say R a b → (pquot.abs R a) = (pquot.abs R b) without mentioning equality +constant pquot.eqv {A : Type} (R : A → A → Prop) {a b : A} : R a b → ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b) +constant pquot.rec {A : Type} {R : A → A → Prop} {C : pquot R → Type} + (f : Π a, C (pquot.abs R a)) + -- sound is essentially saying: ∀ (a b : A) (H : R a b), f a == f b + -- H makes sure we can only define a function on (quot R) if for all a b : A + -- R a b → f a == f b + (sound : ∀ a b, R a b → ∀ P : (Π (q : pquot R), C q → Prop), P (pquot.abs R a) (f a) → P (pquot.abs R b) (f b)) + (q : pquot R) + : C q +-- We would also get the following computational rule: +-- pquot.rec R H₁ H₂ (pquot.abs R a) ==> H₁ a +constant pquot.comp {A : Type} {R : A → A → Prop} {C : pquot R → Type} + (f : Π a, C (pquot.abs R a)) + (sound : ∀ a b, R a b → ∀ P : (Π (q : pquot R), C q → Prop), P (pquot.abs R a) (f a) → P (pquot.abs R b) (f b)) + (a : A) + -- In the implementation this would be a computational rule + : pquot.rec f sound (pquot.abs R a) = f a + +-- If the environment contains = and ==, then we can define + +definition pquot.eq {A : Type} (R : A → A → Prop) {a b : A} (H : R a b) : pquot.abs R a = pquot.abs R b := +have aux : ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b), from + pquot.eqv R H, +aux (λ x : pquot R, pquot.abs R a = x) rfl + +definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type} + (q : pquot R) + (f : Π a, C (pquot.abs R a)) + (sound : ∀ (a b : A), R a b → f a == f b) + : C q := +pquot.rec f + (λ (a b : A) (H : R a b) (P : Π (q : pquot R), C q → Prop) (Ha : P (pquot.abs R a) (f a)), + have aux₁ : f a == f b, from sound a b H, + have aux₂ : pquot.abs R a = pquot.abs R b, from pquot.eq R H, + have aux₃ : ∀ (c₁ c₂ : C (pquot.abs R a)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R a) c₂, from + λ c₁ c₂ e H, eq.rec_on (heq.to_eq e) H, + have aux₄ : ∀ (c₁ : C (pquot.abs R a)) (c₂ : C (pquot.abs R b)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R b) c₂, from + eq.rec_on aux₂ aux₃, + show P (pquot.abs R b) (f b), from + aux₄ (f a) (f b) aux₁ Ha) + q + +definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type} + (f : A → B) + (sound : ∀ (a b : A), R a b → f a = f b) + (q : pquot R) + : B := +pquot.rec_on q f (λ (a b : A) (H : R a b), heq.from_eq (sound a b H)) + +theorem pquot.induction_on {A : Type} {R : A → A → Prop} {P : pquot R → Prop} + (q : pquot R) + (f : ∀ a, P (pquot.abs R a)) + : P q := +pquot.rec_on q f (λ (a b : A) (H : R a b), + have aux₁ : pquot.abs R a = pquot.abs R b, from pquot.eq R H, + have aux₂ : P (pquot.abs R a) = P (pquot.abs R b), from congr_arg P aux₁, + have aux₃ : cast aux₂ (f a) = f b, from proof_irrel (cast aux₂ (f a)) (f b), + show f a == f b, from + @cast_to_heq _ _ _ _ aux₂ aux₃) + +theorem pquot.abs.surjective {A : Type} {R : A → A → Prop} : ∀ q : pquot R, ∃ x : A, pquot.abs R x = q := +take q, pquot.induction_on q (take a, exists_intro a rfl) + +definition pquot.exact {A : Type} (R : A → A → Prop) := +∀ a b : A, pquot.abs R a = pquot.abs R b → R a b + +-- Definable quotient +structure dquot {A : Type} (R : A → A → Prop) := +mk :: (rep : pquot R → A) + (complete : ∀a, R (rep (pquot.abs R a)) a) + -- (stable : ∀q, pquot.abs R (rep q) = q) + +structure is_equiv {A : Type} (R : A → A → Prop) := +mk :: (refl : ∀x, R x x) + (symm : ∀{x y}, R x y → R y x) + (trans : ∀{x y z}, R x y → R y z → R x z) + +-- Definiable quotients are exact if R is an equivalence relation +theorem quot.exact {A : Type} {R : A → A → Prop} (eqv : is_equiv R) (q : dquot R) : pquot.exact R := +λ (a b : A) (H : pquot.abs R a = pquot.abs R b), + have H₁ : pquot.abs R a = pquot.abs R a → R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R a)), + from λH, is_equiv.refl eqv _, + have H₂ : pquot.abs R a = pquot.abs R b → R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R b)), + from eq.subst H H₁, + have H₃ : R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R b)), + from H₂ H, + have H₄ : R a (dquot.rep q (pquot.abs R a)), from is_equiv.symm eqv (dquot.complete q a), + have H₅ : R (dquot.rep q (pquot.abs R b)) b, from dquot.complete q b, + is_equiv.trans eqv H₄ (is_equiv.trans eqv H₃ H₅)