matita/matita/contribs/lambdadelta/nodes
matita/matita/contribs/lambdadelta/token
matita/matita/contribs/lambdadelta/2A1
-matita/matita/contribs/lambdadelta/apps_2/notation
-matita/matita/contribs/lambdadelta/apps_2/models
matita/matita/contribs/lambdadelta/ground_2/xoa/xoa2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation2.ma
matita/matita/contribs/lambdadelta/*/*_probe.txt
--- /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 "apps_2/notation/models/ringeq_4.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].
+
+interpretation "denotational equivalence (model)"
+ 'RingEq M L T1 T2 = (deq M L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma deq_refl (M): is_model M →
+ c_reflexive … (deq M).
+/2 width=1 by mq/ qed.
+(*
+lemma veq_sym: ∀M. symmetric … (veq M).
+// qed-.
+
+theorem veq_trans: ∀M. transitive … (veq M).
+// 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 "ground_2/notation/relations/ringeq_3.ma".
+include "apps_2/notation/models/at_3.ma".
+include "apps_2/notation/models/wbrackets_4.ma".
+include "basic_2/syntax/term.ma".
+
+(* MODEL ********************************************************************)
+
+record model: Type[1] ≝ {
+ dd: Type[0]; (* denotations domain *)
+ sq: relation2 dd dd; (* structural equivalence *)
+ sv: nat → dd; (* sort evaluation *)
+ ap: dd → dd → dd; (* application *)
+ ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *)
+}.
+
+interpretation "structural equivalence (model)"
+ 'RingEq M d1 d2 = (sq M d1 d2).
+
+interpretation "application (model)"
+ 'At M d1 d2 = (ap M d1 d2).
+
+interpretation "term interpretation (model)"
+ 'WBrackets M gv lv T = (ti M gv lv T).
+
+definition evaluation: model → Type[0] ≝ λM. nat → dd 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/syntax/lenv.ma".
+include "apps_2/models/model_push.ma".
+include "apps_2/notation/models/inwbrackets_4.ma".
+
+(* LOCAL ENVIRONMENT INTERPRETATION ****************************************)
+
+inductive li (M) (gv): relation2 lenv (evaluation M) ≝
+| li_atom: ∀lv. li M gv (⋆) lv
+| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] ≗ d → li M gv (L.ⓓV) (⫯[d]lv)
+| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[d]lv)
+| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[d]lv)
+.
+
+interpretation "local environment interpretation (model)"
+ 'InWBrackets M gv L lv = (li M gv L lv).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact li_inv_abbr_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv = v.
+#M #gv #v #Y * -v -Y
+[ #lv #K #W #H destruct
+| #lv #d #L #V #HL #HV #K #W #H destruct /2 width=5 by ex3_2_intro/
+| #lv #d #L #V #_ #K #W #H destruct
+| #lv #d #I #L #_ #K #W #H destruct
+]
+qed-.
+
+lemma li_inv_abbr (M) (gv): ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv = v.
+/2 width=3 by li_inv_abbr_aux/ qed-.
+
+fact li_inv_abst_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v.
+#M #gv #v #Y * -v -Y
+[ #lv #K #U #H destruct
+| #lv #d #L #V #_ #_ #K #U #H destruct
+| #lv #d #L #V #HL #K #U #H destruct /2 width=4 by ex2_2_intro/
+| #lv #d #I #L #_ #K #U #H destruct
+]
+qed-.
+
+lemma li_inv_abst (M) (gv): ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v.
+/2 width=4 by li_inv_abst_aux/ qed-.
+
+fact li_inv_unit_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} →
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v.
+#M #gv #v #Y * -v -Y
+[ #lv #J #K #H destruct
+| #lv #d #L #V #_ #_ #J #K #H destruct
+| #lv #d #L #V #_ #J #K #H destruct
+| #lv #d #I #L #HL #J #K #H destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+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-.
--- /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 "apps_2/models/model_push.ma".
+
+(* MODEL ********************************************************************)
+
+record is_model (M): Prop ≝ {
+ mq: reflexive … (sq M);
+ ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;
+ ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i;
+ mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l;
+ md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv];
+ mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] →
+ (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) →
+ ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2];
+ ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv];
+ me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv];
+ mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv]
+}.
+
+record is_extensional (M): Prop ≝ {
+ mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] →
+ (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) →
+ ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2]
+}.
--- /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 "apps_2/notation/models/upspoon_4.ma".
+include "apps_2/notation/models/upspoon_3.ma".
+include "apps_2/models/model.ma".
+
+(* MODEL ********************************************************************)
+
+definition push (M): nat → dd M → evaluation M → evaluation M ≝
+ λj,d,lv,i. tri … i j (lv i) d (lv (↓i)).
+
+interpretation "generic push (model evaluation)"
+ 'UpSpoon M i d lv = (push M i d lv).
+
+interpretation "push (model evaluation)"
+ 'UpSpoon M d lv = (push M O d lv).
+
+(* Basic properties *********************************************************)
+
+lemma push_lt: ∀M,lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i.
+/2 width=1 by tri_lt/ qed-.
+
+lemma push_eq: ∀M,lv,d,i. (⫯{M}[i←d] lv) i = d.
+/2 width=1 by tri_eq/ qed-.
+
+lemma push_gt: ∀M,lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i).
+/2 width=1 by tri_gt/ 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 "apps_2/models/model_props.ma".
+
+(* EVALUATION EQUIVALENCE **************************************************)
+
+definition veq (M): relation (evaluation M) ≝
+ λv1,v2. ∀d. v1 d ≗ v2 d.
+
+interpretation "evaluation equivalence (model)"
+ 'RingEq M v1 v2 = (veq M v1 v2).
+
+(* Basic properties *********************************************************)
+
+lemma veq_refl (M): is_model M →
+ reflexive … (veq M).
+/2 width=1 by mq/ qed.
+(*
+lemma veq_sym: ∀M. symmetric … (veq M).
+// qed-.
+
+theorem veq_trans: ∀M. transitive … (veq M).
+// qed-.
+*)
\ No newline at end of file
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation < "hvbox( d1 @ break d2 )"
+ right associative with precedence 47
+ for @{ 'At $M $d1 $d2 }.
+
+notation > "hvbox( d1 @ break d2 )"
+ right associative with precedence 47
+ for @{ 'At ? $d1 $d2 }.
+
+notation > "hvbox( d1 @{ break term 46 M } break term 46 d2 )"
+ non associative with precedence 47
+ for @{ 'At $M $d1 $d2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation < "hvbox( lv ϵ ⟦ break term 46 L ⟧[ break term 46 gv ] )"
+ non associative with precedence 45
+ for @{ 'InWBrackets $M $gv $L $lv }.
+
+notation > "hvbox( lv ϵ ⟦ break term 46 L ⟧[ break term 46 gv ] )"
+ non associative with precedence 45
+ for @{ 'InWBrackets ? $gv $L $lv }.
+
+notation > "hvbox( lv ϵ ⟦ break term 46 L ⟧{ break term 46 M }[ break term 46 gv ] )"
+ non associative with precedence 45
+ for @{ 'InWBrackets $M $gv $L $lv }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation < "hvbox( ⫯[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $d $lv }.
+
+notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon ? $d $lv }.
+
+notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $d $lv }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation < "hvbox( ⫯[ term 46 i ← break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $i $d $lv }.
+
+notation > "hvbox( ⫯[ term 46 i ← break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon ? $i $d $lv }.
+
+notation > "hvbox( ⫯{ term 46 M }[ break term 46 i ← break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $i $d $lv }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation < "hvbox( ⟦ term 46 T ⟧[ break term 46 gv, break term 46 lv ] )"
+ non associative with precedence 75
+ for @{ 'WBrackets $M $gv $lv $T }.
+
+notation > "hvbox( ⟦ term 46 T ⟧[ break term 46 gv, break term 46 lv ] )"
+ non associative with precedence 75
+ for @{ 'WBrackets ? $gv $lv $T }.
+
+notation > "hvbox( ⟦ term 46 T ⟧{ break term 46 M }[ break term 46 gv , break term 46 lv ] )"
+ non associative with precedence 75
+ for @{ 'WBrackets $M $gv $lv $T }.
["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
["("; "❨"; "❪"; "❲"; "（"; ];
[")"; "❩"; "❫"; "❳"; "）"; ];
- ["["; "⦋"; "〚"; ] ;
- ["]"; "⦌"; "〛"; ] ;
+ ["["; "⦋"; "⟦"; ] ;
+ ["]"; "⦌"; "⟧"; ] ;
["{"; "❴"; "⦃" ] ;
["}"; "❵"; "⦄" ] ;
["□"; "◽"; "▪"; "◾"; ];
projects / helm.git / commitdiff