matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "apps_2/notation/models/roplus_5.ma".
  16 include "static_2/syntax/lenv.ma".
  17 include "apps_2/models/veq.ma".
  18
  19 (* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************)
  20
  21 inductive vpushs (M) (gv) (lv): relation2 lenv (evaluation M) ≝
  22 | vpushs_atom: vpushs M gv lv (⋆) lv
  23 | vpushs_abbr: ∀v,d,K,V. vpushs M gv lv K v → ⟦V⟧[gv,v] = d → vpushs M gv lv (K.ⓓV) (⫯[0←d]v)
  24 | vpushs_abst: ∀v,d,K,V. vpushs M gv lv K v → vpushs M gv lv (K.ⓛV) (⫯[0←d]v)
  25 | vpushs_unit: ∀v,d,I,K. vpushs M gv lv K v → vpushs M gv lv (K.ⓤ[I]) (⫯[0←d]v)
  26 | vpushs_repl: ∀v1,v2,L. vpushs M gv lv L v1 → v1 ≗ v2 → vpushs M gv lv L v2
  27 .
  28
  29 interpretation "multiple push (model evaluation)"
  30    'ROPlus M gv L lv v  = (vpushs M gv lv L v).
  31
  32 (* Basic inversion lemmas ***************************************************)
  33
  34 fact vpushs_inv_atom_aux (M) (gv) (lv): is_model M →
  35                                         ∀v,L. L ⨁{M}[gv] lv ≘ v →
  36                                         ⋆ = L → lv ≗ v.
  37 #M #gv #lv #HM #v #L #H elim H -v -L
  38 [ #_ /2 width=1 by veq_refl/
  39 | #v #d #K #V #_ #_ #_ #H destruct
  40 | #v #d #K #V #_ #_ #H destruct
  41 | #v #d #I #K #_ #_ #H destruct
  42 | #v1 #v2 #L #_ #Hv12 #IH #H destruct
  43   /3 width=3 by veq_trans/
  44 ]
  45 qed-.
  46
  47 lemma vpushs_inv_atom (M) (gv) (lv): is_model M →
  48                                      ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v.
  49 /2 width=4 by vpushs_inv_atom_aux/ qed-.
  50
  51 fact vpushs_inv_abbr_aux (M) (gv) (lv): is_model M →
  52                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
  53                                         ∀K,V. K.ⓓV = L →
  54                                         ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
  55 #M #gv #lv #HM #y #L #H elim H -y -L
  56 [ #Y #X #H destruct
  57 | #v #d #K #V #Hv #Hd #_ #Y #X #H destruct
  58   /3 width=3 by veq_refl, ex2_intro/
  59 | #v #d #K #V #_ #_ #Y #X #H destruct
  60 | #v #d #I #K #_ #_ #Y #X #H destruct
  61 | #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct
  62   elim IH -IH [|*: // ] #v #Hv #Hv1
  63   /3 width=5 by veq_trans, ex2_intro/
  64 ]
  65 qed-.
  66
  67 lemma vpushs_inv_abbr (M) (gv) (lv): is_model M →
  68                                      ∀y,K,V. K.ⓓV ⨁{M}[gv] lv ≘ y →
  69                                      ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
  70 /2 width=3 by vpushs_inv_abbr_aux/ qed-.
  71
  72 fact vpushs_inv_abst_aux (M) (gv) (lv): is_model M →
  73                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
  74                                         ∀K,W. K.ⓛW = L →
  75                                         ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
  76 #M #gv #lv #HM #y #L #H elim H -y -L
  77 [ #Y #X #H destruct
  78 | #v #d #K #V #_ #_ #_ #Y #X #H destruct
  79 | #v #d #K #V #Hv #_ #Y #X #H destruct
  80   /3 width=4 by veq_refl, ex2_2_intro/
  81 | #v #d #I #K #_ #_ #Y #X #H destruct
  82 | #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct
  83   elim IH -IH [|*: // ] #v #d #Hv #Hv1
  84   /3 width=6 by veq_trans, ex2_2_intro/
  85 ]
  86 qed-.
  87
  88 lemma vpushs_inv_abst (M) (gv) (lv): is_model M →
  89                                      ∀y,K,W. K.ⓛW ⨁{M}[gv] lv ≘ y →
  90                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
  91 /2 width=4 by vpushs_inv_abst_aux/ qed-.
  92
  93 fact vpushs_inv_unit_aux (M) (gv) (lv): is_model M →
  94                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
  95                                         ∀I,K. K.ⓤ[I] = L →
  96                                         ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
  97 #M #gv #lv #HM #y #L #H elim H -y -L
  98 [ #Z #Y #H destruct
  99 | #v #d #K #V #_ #_ #_ #Z #Y #H destruct
 100 | #v #d #K #V #_ #_ #Z #Y #H destruct
 101 | #v #d #I #K #Hv #_ #Z #Y #H destruct
 102   /3 width=4 by veq_refl, ex2_2_intro/
 103 | #v1 #v2 #L #_ #Hv12 #IH #Z #Y #H destruct
 104   elim IH -IH [|*: // ] #v #d #Hv #Hv1
 105   /3 width=6 by veq_trans, ex2_2_intro/
 106 ]
 107 qed-.
 108
 109 lemma vpushs_inv_unit (M) (gv) (lv): is_model M →
 110                                      ∀y,I,K. K.ⓤ[I] ⨁{M}[gv] lv ≘ y →
 111                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
 112 /2 width=4 by vpushs_inv_unit_aux/ qed-.
 113
 114 (* Basic forward lemmas *****************************************************)
 115
 116 lemma vpushs_fwd_bind (M) (gv) (lv): is_model M →
 117                                      ∀y,I,K. K.ⓘ[I] ⨁{M}[gv] lv ≘ y →
 118                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
 119 #M #gv #lv #HM #y * [ #I | * #V ] #L #H
 120 [ /2 width=2 by vpushs_inv_unit/
 121 | elim (vpushs_inv_abbr … H) // -H #v #HL #Hv
 122   /2 width=4 by ex2_2_intro/
 123 | /2 width=2 by vpushs_inv_abst/
 124 ]
 125 qed-.