Skip to content
Snippets Groups Projects
Commit 28e8b2a7 authored by cschoener's avatar cschoener
Browse files

Generalized quotient initial commit.

parent 7bc48457
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
source/casestudies/dhol/dhol.mmt
+ 48
− 40
View file @ 28e8b2a7
......@@ -162,7 +162,7 @@ theory DHOL : ur:?LF =
and_I: {F,G} ⊦F ⟶ ⊦G ⟶ ⊦F∧G ❙
and_El: {F,G} ⊦F∧G ⟶ ⊦F ❙
and_Er: {F,G} ⊦F∧G ⟶ ⊦G ❙
// notation löschen ❙
equivalence: tm ⟶ tm ⟶ tm ❘ # 1 ⇔ 2 ❙
// = [F,G] (F ⇒ G) ∧ (G ⇒ F)❙
......@@ -183,9 +183,14 @@ theory DHOL : ur:?LF =
exists_I: {A,p,x} x%A ⟶ ⊦p x ⟶ ⊦∃ A [y] p y ❙
exists_E: {A,F,p} ⊦(∃ A [x] p x) ⟶ ({x} x%A ⟶ ⊦p x ⟶ ⊦F) ⟶ ⊦F ❙
TND: {F} F%bool ⟶ ⊦F∨¬F ❙
TND: {F} ⊦F∨¬F ❙
bool_ext: {p} ⊦p true ⟶ ⊦p false ⟶ ({x} x%bool ⟶ ⊦p x)❙
contra2: {F} ⊦F∧¬F ⟶ ↯ ❘
= [F,P] falseE valid_eq_flip (and_El P) (and_Er P)❙
classical_neg: {F} (⊦F ⟶ ↯) ⟶ ⊦¬F ❘
= [F,P] or_E TND ([k:⊦F] (P k) ¬F) ([k:⊦¬F] k) ❙
equals_u_is_Pi: {A,u} u%A ⟶ (λ A [x] (x =A u))%(Π A [x] bool) ❘
= [A,u,P] (lam_tp A A ([y] bool) ([y] (y =A u)) eqtp_refl ([y,k:y%A] eq_tp k P)) ❙
equals_u_app_is_bool: {A,t,u} t%A ⟶ u%A ⟶ ((λ A [x] (x =A u)) @ t)%bool❘
......@@ -208,8 +213,8 @@ theory DHOL : ur:?LF =
equivalence_I_trans: {F,G,H,I} ⊦F =bool H ⟶ ⊦G =bool I ⟶ (⊦F⇔G) ⟶ ⊦H⇔I ❘
= [F,G,H,I,P,Q,R] equivalence_I ([k:⊦H] valid_eq_flip (impl_E (equivalence_El R) (valid_eq k P)) Q) ([k:⊦I] valid_eq_flip (impl_E (equivalence_Er R) (valid_eq k Q)) P)❙
// isBinRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tm ❙
// is_BinRel: {A,r,x,y} x%A ⟶ y%A ⟶ r x y % bool ⟶ ⊦isBinRel A r❙
isBinRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ type ❘ role judgment ❘
= [A,r] {x,y} x%A ⟶ y%A ⟶ r x y%bool ❙
// isReflRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tm ❙
// is_ReflRel: {A,r,x} ⊦isBinRel A r ⟶ x%A ⟶ ⊦r x x ⟶ ⊦isReflRel A r❙
// isSymRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tm ❙
......@@ -219,29 +224,34 @@ theory DHOL : ur:?LF =
isEqRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ type ❘ role Judgment ❘
= [A,r] {x,y,z} x%A ⟶ y%A ⟶ z%A ⟶ ⊦(r x x) ∧ (r x y ⇒ r y x) ∧ ((r x y ∧ r y z) ⇒ r x z)❙
isExtension: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ (tm ⟶ tm ⟶ tm) ⟶ type ❘ role Judgment ❘
= [A,r,e] {x,y} x%A ⟶ y%A ⟶ ⊦ r x y ⟶ ⊦ e x y❙
= [A,r,e] {x,y} x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦e x y ❙
isMinExtension: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ (tm ⟶ tm ⟶ tm) ⟶ type ❘ role Judgment ❘
= [A,r,e] {s,x,y} isExtension A r s ⟶ x%A ⟶ y%A ⟶ ⊦¬(s x y) ⟶ ⊦¬(e x y)❙
EqRel_tp: {A,r,x,y} isEqRel A r ⟶ x%A ⟶ y%A ⟶ r x y%bool ❙
EqRel_refl: {A,r,x} isEqRel A r ⟶ x%A ⟶ ⊦r x x ❘
= [A,r,x,P,Q] and_El (and_El (P x x x Q Q Q)) ❙
EqRel_sym: {A,r,x,y} isEqRel A r ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦ r y x ❘
= [A,r,x,y,P,Q,R] and_Er (and_El (P x y x Q R Q)) ❙
EqRel_trans: {A,r,x,y,z} isEqRel A r ⟶ x%A ⟶ y%A ⟶ z%A ⟶ ⊦ r x y ⟶ ⊦ r y z ⟶ ⊦ r x z ❘
= [A,r,x,y,z,P,Q,R,S] and_Er P x y z Q R S ❙
EqRel_sym: {A,r,x,y} isEqRel A r ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦r y x ❘
= [A,r,x,y,P,Q,R,S] impl_E (and_Er (and_El (P x y x Q R Q))) S ❙
EqRel_trans: {A,r,x,y,z} isEqRel A r ⟶ x%A ⟶ y%A ⟶ z%A ⟶ ⊦r x y ∧ r y z ⟶ ⊦r x z ❘
= [A,r,x,y,z,P,Q,R,S,T] impl_E (and_Er P x y z Q R S) T❙
quotient: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tp❘# 1 ∕ 2 prec 5❙
quotient_form: {A,r} ({x,y} x%A ⟶ y%A ⟶ r x y%bool) ⟶ isEqRel A r ⟶ $A∕r ❙
quotient_I: {A,t,r} t%A ⟶ $A∕r ⟶ t%A∕r ❙
quotient_E: {A,B,s,t,r} s%A∕r ⟶ ({x} x%A ⟶ ⊦x =(A∕r) s ⟶ (t x) % (B x)) ⟶ ({x,xˈ} x%A ⟶ xˈ%A ⟶ ⊦x =(A∕r) s ⟶ ⊦xˈ =(A∕r) s ⟶ ⊦(t x) =(B x) (t xˈ)) ⟶ (t s) % (B s) ❙
quotient_eq: {A,s,t,r} s%A ⟶ t%A ⟶ isEqRel A r ⟶ ⊦(s =(A∕r) t) =bool (r s t)❙
// quotient_form: {A,r} ({x,y} x%A ⟶ y%A ⟶ r x y%bool) ⟶ isEqRel A r ⟶ $A∕r ❙
quotient_form: {A,r} isBinRel A r ⟶ $A∕r ❙
quotient_I: {A,x,r} x%A ⟶ $A∕r ⟶ x%A∕r ❙
quotient_E: {A,B,s,t,r} s%A∕r ⟶ ({x} x%A ⟶ ⊦x =(A∕r) s ⟶ (t x) % (B x)) ⟶ ({x,xˈ} x%A ⟶ xˈ%A ⟶ ⊦x =(A∕r) s ⟶ ⊦xˈ =(A∕r) s ⟶ ⊦(t x) =(B x) (t xˈ)) ⟶ (t s) % (B s) ❙
// these two should be used instead of the above if we remove the requirement isEqRel A r from quotient_form❙
// quotient_eq_intro: {A,s,t,r} s%A ⟶ t%A ⟶ ⊦ r s t ⟶ ⊦ s =(A∕r) t❙
// quotient_eq_elim: {A,s,t,r} s%A ⟶ t%A ⟶ ⊦ s =(A∕r) t ⟶
{rˈ} isEqRel A rˈ ⟶ isExtension A r rˈ ⟶ ⊦ rˈ s t❙
quotient_E_quick: {A,B,s,t,r} s%A∕r ⟶ ({x} x%A ⟶ (t x) % (B x)) ⟶ ({x,xˈ} x%A ⟶ xˈ%A ⟶ ⊦ (t x) =(B x) (t xˈ)) ⟶ (t s) % (B s) ❘
= [A,B,s,t,r,P,Q,R] quotient_E P ([x, u: x%A, v: ⊦ x =(A∕r) s] Q x u) ([x, xˈ, u: x%A, v: xˈ%A, k: ⊦ x =(A∕r) s, l: ⊦ xˈ =(A∕r) s] R x xˈ u v) ❙
quotient_eq_I: {A,x,y,r} x%A ⟶ y%A ⟶ isBinRel A r ⟶ ⊦r x y ⟶ ⊦x =(A∕r) y ❙
quotient_eq_E: {A,x,y,r,e} x%A ⟶ y%A ⟶ isExtension A r e ⟶ ⊦x =(A∕r) y ⟶ ⊦e x y❙
quotient_eq_E_neg: {A,x,y,r,e} x%A ⟶ y%A ⟶ isExtension A r e ⟶ ⊦¬(e x y) ⟶ ⊦¬(x =(A∕r) y) ❘
= [A,x,y,r,e,P,Q,R,S] or_E TND ([k:⊦(x =(A∕r) y)] (contra2 (e x y) (and_I (e x y) (¬(e x y)) (quotient_eq_E P Q R k) S)) (¬(x =(A∕r) y))) ([k:⊦¬(x =(A∕r) y)] k) ❙
quotient_eq: {A,r} isMinExtension A r ([x,y] x =(A∕r) y) ❘
= [A,r] [s,x,y, k:isExtension A r s, l:x%A,m:y%A, n:⊦¬(s x y)] quotient_eq_E_neg l m k n
❙
app_sub_eq: {A,B,f,t,tˈ} t%A ⟶ tˈ%A ⟶ ⊦t =A tˈ⟶ ({u} u%A ⟶ (f u) % (B t)) ⟶ ⊦(f t) =(B t) (f tˈ)❘
= [A,B,f,t,tˈ,P,Q,R,S] eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) Q) (S tˈ Q) (eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) P) (app_tp (lam_tp eqtp_refl S) Q) (eq_sym (lam_beta ([k,l:k%A] app_tp (lam_tp eqtp_refl S) l) P)) (app_eq (eq_refl lam_tp eqtp_refl S) R)) (lam_beta ([k,l:k%A] app_tp (lam_tp eqtp_refl S) l) Q)❙
......@@ -251,10 +261,14 @@ theory DHOL : ur:?LF =
singleton_sub: {A,p,s} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ (A|([x] x =A s)) < (A|p)❘
= [A,p,s,P,Q,R] [t:tm, k:t%(A|([x] x =A s))] refine_I (refine_E1 k)
valid_eq_flip R (app_sub_eq A ([x] bool) p s t P (refine_E1 k) (eq_sym (refine_E2 k)) Q)❙
dep_conj_pred_eq_s: {A,s,p} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ({t} t%A ⟶ ((p t ∧ (t =(A|([x] p x)) s))) %bool) ❘
= [A,s,p,P,Q,R] [t,k:t%A] and_tp (Q t k) ([l:⊦p t] eq_tp (refine_I A ([x] p x) t k l) (refine_I A ([x] p x) s P R)) ❙
t_sat_dep_conj_pred_eq_s: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦ (((p t) ∧ (t =(A|([x] p x)) s))) ❘
= [A,s,t,p,P,Q,R,S,T] refine_E2 (t_sat_pred P Q R ([x,k:x%A] dep_conj_pred_eq_s P S T x k) and_I T (eq_refl (refine_I A ([x] p x) s P T))) ❙
= [A,s,t,p,P,Q,R,S,T] refine_E2
(t_sat_pred P Q R
([x,k:x%A] and_tp (S x k) ([l:⊦p x] eq_tp (refine_I A ([x] p x) x k l) (refine_I A ([x] p x) s P T)))
and_I T (eq_refl (refine_I A ([x] p x) s P T)))❙
refine_eq_pres: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦s =(A|p) t ❘
= [A,s,t,p,P,Q,R,S,T] (eq_sym and_Er t_sat_dep_conj_pred_eq_s P Q R S T) ❙
......@@ -282,21 +296,21 @@ theory DHOL : ur:?LF =
ground_type_in_class: {A,r,x,xˈ} $A∕r ⟶ x%A ⟶ xˈ%A ⟶ ⊦(∃ A [y] (y =(A∕r) x)) =(bool|[x] x =bool true) (∃ A [y] (y =(A∕r) xˈ)) ❘
= [A,r,x,xˈ,P,Q,R] both_true_equals (in_class_bool P x Q) (in_class_bool P xˈ R) (in_class_valid P x Q) (in_class_valid P xˈ R)❙
in_class_quo: {A,r,s} $A∕r ⟶ s%A∕r ⟶ ⊦ ∃ A [y] (y =(A∕r) s) ❘
= [A,r,s,P,Q] props_in_true (quotient_E_quick Q ([z,k:z%A] in_class_bool_true A r z P k) ([z,zˈ,k:z%A,l:zˈ%A] ground_type_in_class P k l)) ❙
= [A,r,s,P,Q] props_in_true (quotient_E Q ([z,k:z%A, l] in_class_bool_true A r z P k) ([z,zˈ,k:z%A,l:zˈ%A, m,n] ground_type_in_class P k l)) ❙
quotient_triv: {A} isEqRel A ([x,y] x =A y) ❘
= [A] [x,y,z,k:x%A,l:y%A,m:z%A,] and_I (and_I (eq_refl k) (equivalence_I ([u:⊦x =A y] eq_sym u) ([u:⊦y =A x] eq_sym u))) (impl_I ([u:⊦(x =A y)∧(y =A z)] (eq_trans k l m (and_El u) (and_Er u))))❙
= [A] [x,y,z,k:x%A,l:y%A,m:z%A] and_I (and_I (eq_refl k) (impl_I ([u:⊦x =A y] eq_sym u))) (impl_I ([u:⊦(x =A y)∧(y =A z)] (eq_trans k l m (and_El u) (and_Er u))))❙
quotient_sub: {A,Aˈ,r,rˈ} A<Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y) ⟶ A∕r < Aˈ∕rˈ ❘
= [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E k ([x, l:x%A, m:⊦x=(A∕r) s] quotient_I Aˈ x rˈ (P x l) (quotient_form R)) ([x, xˈ, l:x%A, m:xˈ%A, n:⊦x=(A∕r) s, o:⊦xˈ=(A∕r) s] valid_eq (S x xˈ l m (valid_eq_flip (eq_trans (quotient_I l (quotient_form Q)) k (quotient_I m (quotient_form Q)) n eq_sym o) (quotient_eq l m Q))) (quotient_eq Aˈ x xˈ rˈ (P x l) (P xˈ m) R))❙
= [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E k ([x, l:x%A, m] quotient_I Aˈ x rˈ (P x l) (quotient_form R)) ([x, xˈ, l:x%A, m:xˈ%A, n, o] valid_eq (S x xˈ l m (valid_eq_flip (eq_trans (quotient_I l (quotient_form Q)) k (quotient_I m (quotient_form Q)) n eq_sym o) (quotient_eq l m Q))) (quotient_eq Aˈ x xˈ rˈ (P x l) (P xˈ m) R))❙
quotient_subtp: {A,r} $A∕r ⟶ A < A∕r ❘
= [A,r,P] [x, s: x%A] (quotient_I A x r) s P ❙
two_ary_func_on_quo_help: {A,s,t,r,f} s%A∕r ⟶ t%A ⟶ ({x,y} x%A ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] quotient_E_quick P ([k,l:k%A] R k t l Q) ([k,kˈ,l:k%A,lˈ:kˈ%A] both_true_equalsv (R k t l Q) (R kˈ t lˈ Q))❙
= [A,s,t,r,f,P,Q,R] quotient_E P ([k,l:k%A, m:⊦k=(A∕r)s] R k t l Q) ([k,kˈ,l:k%A,lˈ:kˈ%A, m:⊦k=(A∕r)s,n:⊦kˈ=(A∕r)s] both_true_equalsv (R k t l Q) (R kˈ t lˈ Q))❙
two_ary_func_on_quo_help2: {A,s,t,r,f} s%A∕r ⟶ t%A∕r ⟶ ({x,y} x%A∕r ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] quotient_E_quick Q ([k,l:k%A] R s k P l) ([k,l, m:k%A,n:l%A] both_true_equalsv (R s k P m) (R s l P n))❙
= [A,s,t,r,f,P,Q,R] quotient_E Q ([k,l:k%A, m] R s k P l) ([k,l, m:k%A,n:l%A, o,p] both_true_equalsv (R s k P m) (R s l P n))❙
two_ary_func_on_quo: {A,s,t,r,f} s%A∕r ⟶ t%A∕r ⟶ ({x,y} x%A ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] two_ary_func_on_quo_help2 P Q ([k,l, m:k%A∕r,n:l%A] (two_ary_func_on_quo_help m n R)) ❙
quotient_eqv: {A,s,t,r} s%A∕r ⟶ t%A∕r ⟶ isEqRel A r ⟶ ({x,y} x%A ⟶ y%A ⟶ (r x y)%bool) ⟶ ((s =(A∕r) t) =bool (r s t))%(bool|[x] x =bool true) ❘
......@@ -307,11 +321,11 @@ theory DHOL : ur:?LF =
quotient_eq_triv_quotient: {A} A ≡ A∕([x,y] x=A y) ❘
= [A] subtp_antisym (quotient_subtp (quotient_form quotient_triv)) ([s,k:s%A∕([x,y] x=A y)] quotient_E k ([kˈ,l:kˈ%A,m:⊦kˈ =(A∕([x,y] x=A y)) s] l) ([kˈ,lˈ, m:kˈ%A,n:lˈ%A, o:⊦kˈ =(A∕([x,y] x=A y)) s,p:⊦lˈ =(A∕([x,y] x=A y)) s] valid_eq_flip (eq_trans (quotient_I m (quotient_form quotient_triv)) k (quotient_I n (quotient_form quotient_triv)) o (eq_sym p)) quotient_eq m n quotient_triv)) ❙
quotient_triv_eq: {A,r} isEqRel A r ⟶ isEqRel A ([x,y] x=(A∕r) y) ❘
= [A,r,P] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (eq_refl quotient_I k (quotient_form P)) (equivalence_I ([f:⊦x=(A∕r) y] eq_sym f) ([f:⊦y=(A∕r) x] eq_sym f))) (impl_I ([f:⊦(x=(A∕r) y ∧ y=(A∕r) z)] eq_trans (quotient_I k quotient_form P) (quotient_I l quotient_form P) (quotient_I m quotient_form P) (and_El f) (and_Er f))) ❙
= [A,r,P] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (eq_refl quotient_I k (quotient_form P)) (impl_I ([f:⊦x=(A∕r) y] eq_sym f))) (impl_I ([f:⊦(x=(A∕r) y ∧ y=(A∕r) z)] eq_trans (quotient_I k quotient_form P) (quotient_I l quotient_form P) (quotient_I m quotient_form P) (and_El f) (and_Er f))) ❙
quotient_triv_eq_eq: {A,r} isEqRel A r ⟶ (A∕r) ≡ A∕([x,y] x=(A∕r) y) ❘
= [A,r,P] quotient_eq_rel eqtp_refl P (quotient_triv_eq P) ([x,y, k:x%A,l:y%A] eq_sym quotient_eq k l P ) ❙
EqRel_on_quo: {A,r} isEqRel A r ⟶ isEqRel (A∕r) r ❘
= [A,r,P] [x,y,z, k:x%A∕r,l:y%A∕r,m:z%A∕r] and_I (and_I (valid_eq_flip (eq_refl k) (props_in_true (quotient_eqv A x x r k k P ([s,t, f:s%A,g:t%A] EqRel_tp P f g)))) (equivalence_I ([f:⊦r x y] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A y x r l k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ([f:⊦r y x] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A y x r l k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))))) (impl_I ([f:⊦(r x y)∧(r y z)] valid_eq_flip (eq_trans k l m (valid_eq (and_El f) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h)))) (valid_eq (and_Er f) (props_in_true (quotient_eqv A y z r l m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x z r k m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ❙
= [A,r,P] [x,y,z, k:x%A∕r,l:y%A∕r,m:z%A∕r] and_I (and_I (valid_eq_flip (eq_refl k) (props_in_true (quotient_eqv A x x r k k P ([s,t, f:s%A,g:t%A] EqRel_tp P f g)))) (impl_I ([f:⊦r x y] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A y x r l k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))))) (impl_I ([f:⊦(r x y)∧(r y z)] valid_eq_flip (eq_trans k l m (valid_eq (and_El f) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h)))) (valid_eq (and_Er f) (props_in_true (quotient_eqv A y z r l m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x z r k m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ❙
quotient_idempotent: {A,r} isEqRel A r ⟶ ((A∕r)∕r) ≡ (A∕r) ❘
= [A,r,P] subtp_antisym ([s,k:s%(A∕r)∕r] quotient_E k ([x,l:x%A∕r, m:⊦x=((A∕r)∕r)s] l) ([x,y, l:x%A∕r,m:y%A∕r, n:⊦x=((A∕r)∕r)s,o:⊦y=((A∕r)∕r)s] valid_eq (valid_eq_flip (eq_trans (quotient_I (A∕r) x r l (quotient_form (EqRel_on_quo P))) k (quotient_I (A∕r) y r m (quotient_form (EqRel_on_quo P))) n (eq_sym o)) (quotient_eq (A∕r) x y r l m (EqRel_on_quo P))) (props_in_true (quotient_eqv l m P ([z,w, g:z%A,h:w%A] EqRel_tp P g h))))) (quotient_subtp quotient_form EqRel_on_quo P) ❙
......@@ -320,7 +334,7 @@ theory DHOL : ur:?LF =
= [A,p,pˈ] subtp_antisym ([k,l:k%(A|p)|pˈ] refine_I (refine_E1 refine_E1 l) (and_I (refine_E2 refine_E1 l) (refine_E2 l))) ([k,l:k%A|([x] p x ∧ pˈ x)] refine_I (refine_I (refine_E1 l) (and_El refine_E2 l)) (and_Er refine_E2 l))❙
repeated_quo_help: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ isEqRel A rˈ ❘
= [A,r,rˈ,P,Q] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (EqRel_refl Q (quotient_I k (quotient_form P))) (EqRel_sym Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)))) (EqRel_trans Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) (quotient_I m (quotient_form P)))❙
= [A,r,rˈ,P,Q] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (EqRel_refl Q (quotient_I k (quotient_form P))) (impl_I [u] EqRel_sym Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) u)) (impl_I [u] EqRel_trans Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) (quotient_I m (quotient_form P)) u)❙
repeated_quo_help2: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ A∕rˈ < (A∕r)∕rˈ ❘
= [A,r,rˈ,P,Q] quotient_sub A (A∕r) rˈ rˈ (quotient_subtp quotient_form P) (repeated_quo_help P Q) Q ([x,y, kˈ:x%A,lˈ:y%A, m:⊦rˈ x y] m )❙
repeated_quo_help3: {A,r,rˈ,x,y} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y ❘
......@@ -333,7 +347,7 @@ theory DHOL : ur:?LF =
= [A,r,rˈ,P,Q] subtp_antisym (subtp_trans (repeated_quo_help5 A r rˈ P Q) (eqtp_subtp (quotient_idempotent (repeated_quo_help A r rˈ P Q)))) (repeated_quo_help2 P Q) ❙
quo_in_ref_subtp: {A,r,p} isEqRel A r ⟶ ({x} x%A ⟶ p x%bool) ⟶ isEqRel (A|p) r ❘
= [A,r,p,P,Q] [x,y,z, k:x%A|p,l:y%A|p,m:z%A|p] and_I (and_I (EqRel_refl P (refine_E1 k)) (EqRel_sym P (refine_E1 k) (refine_E1 l))) (EqRel_trans P (refine_E1 k) (refine_E1 l) (refine_E1 m))❙
= [A,r,p,P,Q] [x,y,z, k:x%A|p,l:y%A|p,m:z%A|p] and_I (and_I (EqRel_refl P (refine_E1 k)) (impl_I [u] EqRel_sym P (refine_E1 k) (refine_E1 l) u)) (impl_I [u] EqRel_trans P (refine_E1 k) (refine_E1 l) (refine_E1 m) u)❙
repeated_ref_quo_help: {A,r,p} isEqRel A r ⟶ ({x} x%A∕r ⟶ p x%bool) ⟶ (A∕r)|p < (A|p)∕r ❘
= [A,r,p,P,Q] ([x,k:x%(A∕r)|p] quotient_E (refine_E1 k)
......@@ -424,17 +438,11 @@ theory DHOL : ur:?LF =
forall_I ([b,c:b%A] EqRel_refl (quo_codomain_EqRel c (P b c)) (app_tp k c))
)
(
equivalence_I
impl_I
([a:⊦∀ A [x] (r (f@x) (g@x))]
forall_I ([b, c:b%A]
impl_E
(equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c)))
(forall_E a c)
))
([a:⊦∀ A [x] (r (g@x) (f@x))]
forall_I ([b, c:b%A]
impl_E
(equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp l c) (app_tp k c)))
(impl_I [u] EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c) u)
(forall_E a c)
))
))
......@@ -442,7 +450,7 @@ theory DHOL : ur:?LF =
impl_I
([a:⊦(∀ A [x] (r (f@x) (g@x))) ∧ (∀ A [x] (r (g@x) (h@x)))]
forall_I ([b, c:b%A]
impl_E (EqRel_trans (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c) (app_tp m c))
impl_E (impl_I [u] EqRel_trans (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c) (app_tp m c) u)
(and_I (forall_E (and_El a) c) (forall_E (and_Er a) c))
))
)
......
source/casestudies/dhol/dhol_generalized_quotient.mmt 0 → 100644
+ 517
− 0
View file @ 28e8b2a7
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment