1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "apps_2/models/model_vlift.ma".
17 (* MODEL ********************************************************************)
19 record is_model (M): Prop ≝ {
20 mq: reflexive … (sq M);
21 mr: replace_2 … (sq M) (sq M) (sq M);
22 mc: compatible_3 … (ap M) (sq M) (sq M) (sq M);
23 ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;
24 ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i;
25 mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l;
26 md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv];
27 mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] →
28 (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) →
29 ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2];
30 ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv];
31 me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv];
32 mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv]
35 record is_extensional (M): Prop ≝ {
36 mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] →
37 (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) →
38 ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2]
41 (* Basic properties *********************************************************)
43 lemma seq_sym (M): is_model M → symmetric … (sq M).
44 /3 width=5 by mr, mq/ qed-.
46 lemma seq_trans (M): is_model M → Transitive … (sq M).
47 /3 width=5 by mr, mq/ qed-.
49 lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M).
50 /3 width=3 by seq_trans, seq_sym/ qed-.
52 lemma seq_canc_dx (M): is_model M → right_cancellable … (sq M).
53 /3 width=3 by seq_trans, seq_sym/ qed-.
55 lemma ti_lref_vlift_eq (M): is_model M →
56 ∀gv,lv,d,i. ⟦#i⟧[gv,⫯[i←d]lv] ≗{M} d.
58 @(seq_trans … HM) [2: @ml // | skip ]
59 >vlift_eq /2 width=1 by mq/
62 lemma ti_lref_vlift_gt (M): is_model M →
63 ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[d]lv] ≗{M} ⟦#i⟧[gv,lv].
65 @(mr … HM) [4,5: @(seq_sym … HM) @(ml … HM) |1,2: skip ]
66 >vlift_gt /2 width=1 by mq/