matita/matita/contribs/lambdadelta/static_2/static/feqg.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 "static_2/notation/relations/stareqsn_7.ma".
  16 include "static_2/syntax/genv.ma".
  17 include "static_2/static/reqg.ma".
  18
  19 (* GENERIC EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *********************)
  20
  21 inductive feqg (S) (G) (L1) (T1): relation3 genv lenv term ≝
  22 | feqg_intro_sn: ∀L2,T2. L1 ≛[S,T1] L2 → T1 ≛[S] T2 →
  23                  feqg S G L1 T1 G L2 T2
  24 .
  25
  26 interpretation
  27   "generic equivalence on referred entries (closure)"
  28   'StarEqSn S G1 L1 T1 G2 L2 T2 = (feqg S G1 L1 T1 G2 L2 T2).
  29
  30 (* Basic_properties *********************************************************)
  31
  32 lemma feqg_intro_dx (S) (G):
  33       reflexive … S → symmetric … S →
  34       ∀L1,L2,T2. L1 ≛[S,T2] L2 →
  35       ∀T1. T1 ≛[S] T2 → ❨G,L1,T1❩ ≛[S] ❨G,L2,T2❩.
  36 /3 width=6 by feqg_intro_sn, teqg_reqg_div/ qed.
  37
  38 (* Basic inversion lemmas ***************************************************)
  39
  40 lemma feqg_inv_gen_sn (S):
  41       ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ →
  42       ∧∧ G1 = G2 & L1 ≛[S,T1] L2 & T1 ≛[S] T2.
  43 #S #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
  44 qed-.
  45
  46 lemma feqg_inv_gen_dx (S):
  47       reflexive … S →
  48       ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ →
  49       ∧∧ G1 = G2 & L1 ≛[S,T2] L2 & T1 ≛[S] T2.
  50 #S #HS #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
  51 /3 width=6 by teqg_reqg_conf_sn, and3_intro/
  52 qed-.
  53
  54 (* Basic forward lemmas *****************************************************)
  55
  56 lemma feqg_fwd_teqg (S):
  57       ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → T1 ≛[S] T2.
  58 #S #G1 #G2 #L1 #L2 #T1 #T2 #H
  59 elim (feqg_inv_gen_sn … H) -H //
  60 qed-.
  61
  62 lemma feqg_fwd_reqg_sn (S):
  63       ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → L1 ≛[S,T1] L2.
  64 #S #G1 #G2 #L1 #L2 #T1 #T2 #H
  65 elim (feqg_inv_gen_sn … H) -H //
  66 qed-.
  67
  68 lemma feqg_fwd_reqg_dx (S):
  69       reflexive … S →
  70       ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → L1 ≛[S,T2] L2.
  71 #S #HS #G1 #G2 #L1 #L2 #T1 #T2 #H
  72 elim (feqg_inv_gen_dx … H) -H //
  73 qed-.
  74
  75 (* Basic_2A1: removed theorems 6:
  76               fleq_refl fleq_sym fleq_inv_gen
  77               fleq_trans fleq_canc_sn fleq_canc_dx
  78 *)