matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.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 "ground_2/lib/functions.ma".
  16 include "ground_2/lib/exteq.ma".
  17 include "apps_2/models/tm.ma".
  18
  19 (* TERM MODEL ***************************************************************)
  20
  21 (* Properties with extensional equivalencs of evaluations *******************)
  22
  23 lemma tm_gc_id: ∀j. ⇡[j]tm_gc ≐ tm_gc.
  24 // qed.
  25
  26 lemma tm_lc_id: ⇡[0←#0]tm_lc ≐ tm_lc.
  27 #i elim (eq_or_gt i) #Hi destruct //
  28 >tm_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
  29 qed.
  30
  31 lemma tm_vlift_comp (l): compatible_2 … (tm_vlift l) (exteq …) (exteq …).
  32 #l #gv1 #gv2 #Hgv #i
  33 >tm_vlift_rw >tm_vlift_rw //
  34 qed.
  35
  36 lemma tm_vpush_comp (i): compatible_3 … (tm_vpush i) (eq …) (exteq …) (exteq …).
  37 #i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
  38 elim (lt_or_eq_or_gt j i) #Hij destruct
  39 [ >tm_vpush_lt // >tm_vpush_lt //
  40 | >tm_vpush_eq >tm_vpush_eq //
  41 | >tm_vpush_gt // >tm_vpush_gt //
  42 ]
  43 qed-.
  44
  45 lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exteq …) (eq …).
  46 #T elim T -T *
  47 [ //
  48 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
  49   whd in ⊢ (??%%); //
  50 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
  51   whd in ⊢ (??%%); //
  52 | #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
  53   whd in ⊢ (??%%); /4 width=1 by tm_vlift_comp, tm_vpush_comp, eq_f3/
  54 | #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
  55   whd in ⊢ (??%%); /3 width=1 by eq_f3/
  56 ]
  57 qed-.
  58
  59 lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T.
  60 #T elim T -T * //
  61 [ #p #I #V #T #IHV #IHT
  62   <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
  63   whd in ⊢ (??%?); /3 width=1 by tm_ti_comp, eq_f3/
  64 | #I #V #T #IHV #IHT
  65   <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
  66 ]
  67 qed.