]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
update in apps_2
[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / veq.ma
1
2 (**************************************************************************)
3 (*       ___                                                              *)
4 (*      ||M||                                                             *)
5 (*      ||A||       A project by Andrea Asperti                           *)
6 (*      ||T||                                                             *)
7 (*      ||I||       Developers:                                           *)
8 (*      ||T||         The HELM team.                                      *)
9 (*      ||A||         http://helm.cs.unibo.it                             *)
10 (*      \   /                                                             *)
11 (*       \ /        This file is distributed under the terms of the       *)
12 (*        v         GNU General Public License Version 2                  *)
13 (*                                                                        *)
14 (**************************************************************************)
15
16 include "apps_2/models/model_props.ma".
17
18 (* EVALUATION EQUIVALENCE ***************************************************)
19
20 definition veq (M): relation (evaluation M) ≝
21                     λv1,v2. ∀d. v1 d ≗ v2 d.
22
23 interpretation "evaluation equivalence (model)"
24    'RingEq M v1 v2 = (veq M v1 v2).
25
26 (* Basic properties *********************************************************)
27
28 lemma veq_refl (M): is_model M →
29                     reflexive … (veq M).
30 /2 width=1 by mr/ qed.
31
32 lemma veq_repl (M): is_model M →
33                     replace_2 … (veq M) (veq M) (veq M).
34 /2 width=5 by mq/ qed-.
35
36 lemma veq_sym (M): is_model M → symmetric … (veq M).
37 /3 width=5 by veq_repl, veq_refl/ qed-.
38
39 lemma veq_trans (M): is_model M → Transitive … (veq M).
40 /3 width=5 by veq_repl, veq_refl/ qed-.
41
42 lemma veq_canc_sn (M): is_model M → left_cancellable … (veq M).
43 /3 width=3 by veq_trans, veq_sym/ qed-.
44
45 lemma veq_canc_dx (M): is_model M → right_cancellable … (veq M).
46 /3 width=3 by veq_trans, veq_sym/ qed-.
47
48 (* Properties with evaluation push ******************************************)
49
50 theorem vpush_swap (M): is_model M →
51                         ∀i1,i2. i1 ≤ i2 →
52                         ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≗{M} ⫯[↑i2←d2] ⫯[i1←d1] lv.
53 #M #HM #i1 #i2 #Hi12 #lv #d1 #d2 #j
54 elim (lt_or_eq_or_gt j i1) #Hji1 destruct
55 [ lapply (lt_to_le_to_lt … Hji1 Hi12) #Hji2
56   >vpush_lt // >vpush_lt // >vpush_lt /2 width=1 by lt_S/ >vpush_lt //
57   /2 width=1 by veq_refl/
58 | >vpush_eq >vpush_lt /2 width=1 by monotonic_le_plus_l/ >vpush_eq
59   /2 width=1 by mr/
60 | >vpush_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct
61   [ >vpush_lt // >vpush_lt /2 width=1 by lt_minus_to_plus/ >vpush_gt //
62     /2 width=1 by veq_refl/
63   | >vpush_eq <(lt_succ_pred … Hji1) >vpush_eq
64     /2 width=1 by mr/
65   | lapply (le_to_lt_to_lt … Hi12 Hji2) #Hi1j
66     >vpush_gt // >vpush_gt /2 width=1 by lt_minus_to_plus_r/ >vpush_gt //
67     /2 width=1 by veq_refl/
68   ]
69 ]
70 qed.
71
72 lemma vpush_comp (M): is_model M →
73                       ∀i. compatible_3 … (vpush M i) (sq M) (veq M) (veq M).
74 #M #HM #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j
75 elim (lt_or_eq_or_gt j i) #Hij destruct
76 [ >vpush_lt // >vpush_lt //
77 | >vpush_eq >vpush_eq //
78 | >vpush_gt // >vpush_gt //
79 ]
80 qed-.
81
82 (* Properies with term interpretation ***************************************) 
83
84 lemma ti_comp (M): is_model M →
85                    ∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 →
86                    ⟦T⟧[gv1, lv1] ≗{M} ⟦T⟧[gv2, lv2].
87 #M #HM #T elim T -T * [||| #p * | * ]
88 [ /4 width=5 by seq_trans, seq_sym, ms/
89 | /4 width=5 by seq_sym, ml, mq/
90 | /4 width=3 by seq_trans, seq_sym, mg/
91 | /6 width=5 by vpush_comp, seq_sym, md, mc, mq/
92 | /5 width=1 by vpush_comp, mi, mr/
93 | /4 width=5 by seq_sym, ma, mp, mq/
94 | /4 width=5 by seq_sym, me, mq/
95 ]
96 qed.