matita/matita/contribs/lambdadelta/basic_2/syntax/bind_ext2.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 "basic_2/syntax/bind.ma".
  16
  17 (* EXTENSION TO BINDERS OF A RELATION FOR TERMS *****************************)
  18
  19 inductive ext2 (R:relation term): relation bind ≝
  20 | ext2_unit: ∀I. ext2 R (BUnit I) (BUnit I)
  21 | ext2_pair: ∀I,V1,V2. R V1 V2 → ext2 R (BPair I V1) (BPair I V2)
  22 .
  23
  24 (* Basic_inversion lemmas **************************************************)
  25
  26 fact ext2_inv_unit_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
  27                            ∀I. Z1 = BUnit I → Z2 = BUnit I.
  28 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
  29 #J #H destruct //
  30 qed-.
  31
  32 lemma ext2_inv_unit_sn: ∀R,I,Z2. ext2 R (BUnit I) Z2 → Z2 = BUnit I.
  33 /2 width=4 by ext2_inv_unit_sn_aux/ qed-.
  34
  35 fact ext2_inv_pair_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
  36                            ∀I,V1. Z1 = BPair I V1 →
  37                            ∃∃V2. R V1 V2 & Z2 = BPair I V2.
  38 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
  39 #J #W1 #H destruct /2 width=3 by ex2_intro/
  40 qed-.
  41
  42 lemma ext2_inv_pair_sn: ∀R,Z2,I,V1. ext2 R (BPair I V1) Z2 →
  43                         ∃∃V2. R V1 V2 & Z2 = BPair I V2.
  44 /2 width=3 by ext2_inv_pair_sn_aux/ qed-.
  45
  46 fact ext2_inv_unit_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
  47                            ∀I. Z2 = BUnit I → Z1 = BUnit I.
  48 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
  49 #J #H destruct //
  50 qed-.
  51
  52 lemma ext2_inv_unit_dx: ∀R,I,Z1. ext2 R Z1 (BUnit I) → Z1 = BUnit I.
  53 /2 width=4 by ext2_inv_unit_dx_aux/ qed-.
  54
  55 fact ext2_inv_pair_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
  56                            ∀I,V2. Z2 = BPair I V2 →
  57                            ∃∃V1. R V1 V2 & Z1 = BPair I V1.
  58 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
  59 #J #W2 #H destruct /2 width=3 by ex2_intro/
  60 qed-.
  61
  62 lemma ext2_inv_pair_dx: ∀R,Z1,I,V2. ext2 R Z1 (BPair I V2) →
  63                         ∃∃V1. R V1 V2 & Z1 = BPair I V1.
  64 /2 width=3 by ext2_inv_pair_dx_aux/ qed-.
  65
  66 (* Basic properties ********************************************************)
  67
  68 lemma ext2_refl: ∀R. reflexive … R → reflexive … (ext2 R).
  69 #R #HR * /2 width=1 by ext2_pair/
  70 qed.
  71
  72 lemma ext2_sym: ∀R. symmetric … R → symmetric … (ext2 R).
  73 #R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/
  74 qed-.