+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpr.ma".
-include "apps_2/models/model_drop.ma".
-
-(* MODEL ********************************************************************)
-
-(* Forward lemmas on context-sensitive parallel reduction for terms *********)
-
-lemma sound_fwd_cpr: ∀M. sound M → extensional M →
- ∀sv,gv,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 →
- ∀lv. lv ∈ 〚L〛⦋M⦌{sv, gv} → 〚T1〛{sv, gv, lv} = 〚T2〛{sv, gv, lv}.
-#M #H1M #H2M #sv #gv #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #lv #Hlv >(m2 … H1M)
- <(sound_fwd_lift … H1M H2M … HVW2) -HVW2
- lapply (sound_drop … HLK … Hlv) // -L -H2M #H
- elim (li_inv_ldef … H) -H #v #HK #H
- elim (lower_inv_raise_be … H) -H #H >H -H #Hlv
- <IHV12 -IHV12 /3 width=3 by sound_ti_eq_l, li_veq, veq_sym/
-| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #lv #Hlv
- [ >(m4 … H1M) >(m4 … H1M) -H1M <IHV12 -IHV12 /3 width=1 by li_ldef/
- | @(mx … H2M) -H2M /3 width=1 by li_ldec/
- ]
-| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #lv #Hlv
- [ >(m6 … H1M) >(m6 … H1M) -H1M /3 width=1 by eq_f2/
- | -IHV12 >(m7 … H1M) >(m7 … H1M) -H1M /2 width=1 by/
- ]
-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #lv #Hlv >(m4 … H1M)
- >IHU12 -IHU12 /2 width=1 by li_ldef/
- <(sound_fwd_lift … H1M H2M … HTU2) -H2M -HTU2
- /2 width=1 by sound_ti_eq_l/
-| #G #L #V #T1 #T2 #_ #IHT12 #lv #Hlv >(m7 … H1M) -H1M /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #w2 #T1 #T2 #_ #_ #_ #IHV12 #_ #IHT12 #lv #Hlv
- >(m6 … H1M) >(m8 … H1M) >(m4 … H1M) >(m7 … H1M) -H1M
- >IHV12 -IHV12 /3 width=1 by li_ldec/
-| #a #G #L #V1 #V2 #W2 #U1 #U2 #T1 #T2 #_ #HVW2 #_ #_ #IHV12 #IHU12 #IHT12 #lv #Hlv
- >(m6 … H1M) >(m4 … H1M) >(m4 … H1M) >(m6 … H1M)
- >IHV12 -IHV12 // <IHU12 -IHU12 // @eq_f2 /3 width=1 by li_ldef/
- <(sound_fwd_lift … H1M H2M … HVW2) -H2M -HVW2
- /2 width=1 by sound_ti_eq_l/
-]
-qed-.
(* *)
(**************************************************************************)
-include "apps_2/notation/models/ringeq_4.ma".
+include "apps_2/notation/models/ringeq_5.ma".
+include "apps_2/models/model_gi.ma".
include "apps_2/models/model_li.ma".
include "apps_2/models/model_props.ma".
(* DENOTATIONAL EQUIVALENCE ************************************************)
-definition deq (M): relation3 lenv term term ≝
- λL,T1,T2. ∀gv,lv. lv ϵ ⟦L⟧[gv] → ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, lv].
+definition deq (M): relation4 genv lenv term term ≝
+ λG,L,T1,T2. ∀gv,lv. lv ϵ ⟦L⟧[gv] → ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, lv].
interpretation "denotational equivalence (model)"
- 'RingEq M L T1 T2 = (deq M L T1 T2).
+ 'RingEq M G L T1 T2 = (deq M G L T1 T2).
(* Basic properties *********************************************************)
lemma deq_refl (M): is_model M →
- c_reflexive … (deq M).
+ ∀G,L. reflexive … (deq M G L).
/2 width=1 by mq/ qed.
(*
lemma veq_sym: ∀M. symmetric … (veq M).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/cpr.ma".
+include "apps_2/models/veq_lifts.ma".
+include "apps_2/models/deq.ma".
+
+(* DENOTATIONAL EQUIVALENCE ************************************************)
+
+(* Forward lemmas with context-sensitive parallel reduction for terms *******)
+
+lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M →
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ≗{M} T2.
+#h #M #H1M #H2M #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2
+[ /2 width=2 by deq_refl/
+| #G #K #V1 #V2 #W2 #_ #IH #HVW2 #gv #v #H
+ elim (li_inv_abbr … H) -H #lv #d #HK #Hd #H
+ @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v
+ lapply (lifts_SO_fwd_vlift … gv H1M H2M … HVW2 lv d) -HVW2 #HVW2
+ @(seq_trans … H1M … HVW2) -W2
+ @(seq_trans … H1M) [3: @IH // | skip ] -G -K -V2
+ @(seq_canc_dx … H1M … Hd) -V1 /2 width=1 by ti_lref_vlift_eq/
+| #I #G #K #T #U #i #_ #IH #HTU #gv #v #H
+ elim (li_fwd_bind … H) -H #lv #d #HK #H
+ @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v
+ lapply (lifts_SO_fwd_vlift … gv H1M H2M … HTU lv d) -HTU #HTU
+ @(seq_trans … H1M … HTU) -U
+ @(seq_trans … H1M) [3: @IH // | skip ] -G -K -T
+ /2 width=1 by ti_lref_vlift_gt/
+| #p * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv
+ [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ] -p
+ @(seq_trans … H1M) [3: @IHT /3 width=1 by li_abbr/ | skip ] -T2
+ /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+ | @(mx … H2M) /3 width=1 by li_abst/
+ ]
+| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv
+ [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(ma … H1M) |1,2: skip ]
+ /3 width=1 by mc/
+ | @(mr … H1M) [4,5: @(seq_sym … H1M) @(me … H1M) |1,2: skip ]
+ /2 width=1 by/
+ ]
+| #G #L #V #U1 #U2 #T2 #_ #IH #HTU2 #gv #lv #Hlv
+ @(seq_trans … H1M) [2: @(md … H1M) | skip ]
+ @(seq_trans … H1M) [2: @IH /3 width=1 by li_abbr, veq_refl/ | skip ] -G -L -U1
+ /3 width=1 by lifts_SO_fwd_vlift, seq_sym/
+| #G #L #V #T1 #T2 #_ #IH #gv #lv #Hlv
+ @(seq_trans … H1M) [2: @(me … H1M) | skip ]
+ /2 width=1 by/
+| #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #_ #IHT #gv #lv #Hlv
+ @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ]
+ @(seq_trans … H1M) [3: @IHT /2 width=1 by li_abst/ | skip ] -T2
+ @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mb … H1M) | @(ti_comp_l … H1M) ] |1,2: skip ]
+ [2: @vlift_comp [2: @(me … H1M) |4: @(veq_refl … H1M) |1,3: skip ] | skip ]
+ /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+| #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv
+ @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ]
+ @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mc … H1M) | @(ma … H1M) ] |1,2: skip ]
+ [2: @IHV // |4: @(md … H1M) |1,3: skip ] -p -V1
+ @(mc … H1M) [ /2 width=1 by lifts_SO_fwd_vlift/ ] -V -V2
+ @(seq_trans … H1M) [2: @IHT /3 width=1 by li_abbr, veq_refl/ | skip ] -T1
+ /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/syntax/genv.ma".
+
+(* GLOBAL ENVIRONMENT INTERPRETATION ***************************************)
lemma li_inv_unit (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] →
∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
/2 width=4 by li_inv_unit_aux/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma li_fwd_bind (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
+#m #gv #v * [ #I | * #V ] #L #H
+[ @(li_inv_unit … H)
+| elim (li_inv_abbr … H) -H #lv #d #Hl #_ #Hv
+ /2 width=4 by ex2_2_intro/
+| @(li_inv_abst … H)
+]
+qed-.
lemma seq_trans (M): is_model M → Transitive … (sq M).
/3 width=5 by mr, mq/ qed-.
+
+lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M).
+/3 width=3 by seq_trans, seq_sym/ qed-.
+
+lemma seq_canc_dx (M): is_model M → right_cancellable … (sq M).
+/3 width=3 by seq_trans, seq_sym/ qed-.
+
+lemma ti_lref_vlift_eq (M): is_model M →
+ ∀gv,lv,d,i. ⟦#i⟧[gv,⫯[i←d]lv] ≗{M} d.
+#M #HM #gv #lv #d #i
+@(seq_trans … HM) [2: @ml // | skip ]
+>vlift_eq /2 width=1 by mq/
+qed.
+
+lemma ti_lref_vlift_gt (M): is_model M →
+ ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[d]lv] ≗{M} ⟦#i⟧[gv,lv].
+#M #HM #gv #lv #d #i
+@(mr … HM) [4,5: @(seq_sym … HM) @(ml … HM) |1,2: skip ]
+>vlift_gt /2 width=1 by mq/
+qed.
replace_2 … (veq M) (veq M) (veq M).
/2 width=5 by mr/ qed-.
+lemma veq_sym (M): is_model M → symmetric … (veq M).
+/3 width=5 by veq_repl, veq_refl/ qed-.
+
+lemma veq_trans (M): is_model M → Transitive … (veq M).
+/3 width=5 by veq_repl, veq_refl/ qed-.
+
+(* Properties with extebsional equivalence **********************************)
+
lemma ext_veq (M): is_model M →
∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2.
/2 width=1 by mq/ qed.
+lemma veq_repl_exteq (M): is_model M →
+ replace_2 … (veq M) (exteq …) (exteq …).
+/2 width=5 by mr/ qed-.
+
lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv →
∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2.
// qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation < "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RingEq $M $L $T1 $T2 }.
-
-notation > "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RingEq ? $L $T1 $T2 }.
-
-notation > "hvbox( L ⊢ break term 46 T1 ≗{ break term 46 M } break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RingEq $M $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RingEq $M $G $L $T1 $T2 }.
+
+notation > "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RingEq ? $G $L $T1 $T2 }.
+
+notation > "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗{ break term 46 M } break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RingEq $M $G $L $T1 $T2 }.
class "orange"
[ { "models" * } {
[ { "denotational equivalence" * } {
- [ "deq" + "( ? ⊢ ? ≗{?} ? )" * ]
+ [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
}
]
[ { "evaluation equivalence" * } {
"model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )"
"model_props"
"model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
+ "model_gi"
* ]
}
]
]
qed-.
+(* Basic eliminators ********************************************************)
+
+lemma cpr_ind (h): ∀R:relation4 genv lenv term term.
+ (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
+ (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → R G K V1 V2 →
+ ⬆*[1] V2 ≘ W2 → R G (K.ⓓV1) (#0) W2
+ ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → R G K (#i) T →
+ ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U)
+ ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 →
+ R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
+ R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → R G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2
+ ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2 →
+ R G L (ⓝV.T1) T2
+ ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 →
+ R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
+ R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 →
+ R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
+ ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ ) →
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2.
+#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
+* #c #HC #H generalize in match HC; -HC
+elim H -c -G -L -T1 -T2
+[ /2 width=3 by ex2_intro/
+| #G #L #s #H
+ lapply (isrt_inv_01 … H) -H #H destruct
+| /3 width=4 by ex2_intro/
+| #c #G #L #V1 #V2 #W2 #_ #_ #_ #H
+ elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct
+| /3 width=4 by ex2_intro/
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H
+ elim (isrt_O_inv_max … H) -H #HcV #HcT
+ /4 width=3 by isr_inv_shift, ex2_intro/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H
+ elim (isrt_O_inv_max … H) -H #HcV #HcT
+ /4 width=3 by isr_inv_shift, ex2_intro/
+| #cU #cT #G #L #U1 #U2 #T1 #T2 #HUT #HU12 #HT12 #IHU #IHT #H
+ elim (isrt_O_inv_max … H) -H #HcV #HcT
+ /3 width=3 by ex2_intro/
+| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/
+| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/
+| #c #G #L #U1 #U2 #T #_ #_ #H
+ elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #IHV #IHW #IHT #H
+ lapply (isrt_inv_plus_O_dx … H ?) -H // #H
+ elim (isrt_O_inv_max … H) -H #H #HcT
+ elim (isrt_O_inv_max … H) -H #HcV #HcW
+ /4 width=3 by isr_inv_shift, ex2_intro/
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #IHV #IHW #IHT #H
+ lapply (isrt_inv_plus_O_dx … H ?) -H // #H
+ elim (isrt_O_inv_max … H) -H #H #HcT
+ elim (isrt_O_inv_max … H) -H #HcV #HcW
+ /4 width=4 by isr_inv_shift, ex2_intro/
+]
+qed-.
+
(* Basic_1: removed theorems 12:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
pr0_delta1
-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
elim (max_inv_O3 … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
qed-.
+lemma isrt_O_inv_max: ∀c1,c2. 𝐑𝐓⦃0, c1 ∨ c2⦄ → ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃0, c2⦄.
+#c1 #c2 #H
+elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H
+elim (max_inv_O3 … H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
lemma isrt_inv_max_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
#n #c1 #c2 #H #H2
elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
projects / helm.git / commitdiff