matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.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/relocation/pr_sle.ma".
  16 (* * this should go first *)
  17 include "ground/relocation/pr_tl_eq.ma".
  18
  19 (* INCLUSION FOR PARTIAL RELOCATION MAPS ************************************)
  20
  21 (* Constructions with pr_eq *************************************************)
  22
  23 (*** sle_eq_repl_back1 *)
  24 corec lemma pr_sle_eq_repl_back_sn:
  25             ∀f2:pr_map. pr_eq_repl_back … (λf1:pr_map. f1 ⊆ f2).
  26 #f2 #f1 * -f2 -f1
  27 #f1 #f2 #g1 #g2 #Hf #H1 #H2 #g #H0
  28 [ cases (pr_eq_inv_push_sn …  H0 …  H1) -g1 /3 width=5 by pr_sle_push/
  29 | cases (pr_eq_inv_next_sn …  H0 …  H1) -g1 /3 width=5 by pr_sle_next/
  30 | cases (pr_eq_inv_push_sn …  H0 …  H1) -g1 /3 width=5 by pr_sle_weak/
  31 ]
  32 qed-.
  33
  34 (*** sle_eq_repl_fwd1 *)
  35 lemma pr_sle_eq_repl_fwd_sn:
  36       ∀f2. pr_eq_repl_fwd … (λf1. f1 ⊆ f2).
  37 #f2 @pr_eq_repl_sym /2 width=3 by pr_sle_eq_repl_back_sn/
  38 qed-.
  39
  40 (*** sle_eq_repl_back2 *)
  41 corec lemma pr_sle_eq_repl_back_dx:
  42             ∀f1. pr_eq_repl_back … (λf2. f1 ⊆ f2).
  43 #f1 #f2 * -f1 -f2
  44 #f1 #f2 #g1 #g2 #Hf #H1 #H2 #g #H0
  45 [ cases (pr_eq_inv_push_sn …  H0 …  H2) -g2 /3 width=5 by pr_sle_push/
  46 | cases (pr_eq_inv_next_sn …  H0 …  H2) -g2 /3 width=5 by pr_sle_next/
  47 | cases (pr_eq_inv_next_sn …  H0 …  H2) -g2 /3 width=5 by pr_sle_weak/
  48 ]
  49 qed-.
  50
  51 (*** sle_eq_repl_fwd2 *)
  52 lemma pr_sle_eq_repl_fwd_dx:
  53       ∀f1. pr_eq_repl_fwd … (λf2. f1 ⊆ f2).
  54 #f1 @pr_eq_repl_sym /2 width=3 by pr_sle_eq_repl_back_dx/
  55 qed-.
  56
  57 (*** sle_refl_eq *)
  58 lemma pr_sle_refl_eq:
  59       ∀f1,f2. f1 ≡ f2 → f1 ⊆ f2.
  60 /2 width=3 by pr_sle_eq_repl_back_dx/ qed.