helm/software/matita/nlibrary/datatypes/pairs-setoids.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 "datatypes/pairs.ma".
  16 include "sets/setoids.ma".
  17
  18 nlet rec eq_pair (A, B : setoid) (a : A × B) (b : A × B) on a : CProp[0] ≝
  19   match a with [ mk_pair a1 a2 ⇒
  20   match b with [ mk_pair b1 b2 ⇒ a1 = b1 ∧ a2 = b2 ]].
  21
  22 interpretation "eq_pair" 'eq_low a b = (eq_pair ?? a b).
  23
  24 nlemma PAIR : ∀A,B:setoid. setoid.
  25 #A B; @(A × B); @(eq_pair …);
  26 ##[ #ab; ncases ab; #a b; @; napply #;
  27 ##| #ab cd; ncases ab; ncases cd; #a1 a2 b1 b2; *; #E1 E2;
  28     @; napply (?^-1); //;
  29 ##| #a b c; ncases a; ncases b; ncases c; #c1 c2 b1 b2 a1 a2;
  30     *; #E1 E2; *; #E3 E4; @; ##[ napply (.= E1); //] napply (.= E2); //.##]
  31 nqed.
  32
  33 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
  34 unification hint 0 ≔ AA, BB;
  35     A ≟ carr AA, B ≟ carr BB,
  36     P1 ≟ refl ? (eq0 (PAIR AA BB)),
  37     P2 ≟ sym ? (eq0 (PAIR AA BB)),
  38     P3 ≟ trans ? (eq0 (PAIR AA BB)),
  39     R ≟ mk_setoid (A × B) (mk_equivalence_relation ? (eq_pair …) P1 P2 P3)
  40 (*---------------------------------------------------------------------------*)⊢
  41     carr R ≡ A × B.
  42
  43 unification hint 0 ≔ S1,S2,a,b;
  44    R ≟ PAIR S1 S2,
  45    L ≟ pair (carr S1) (carr S2)
  46 (* -------------------------------------------- *) ⊢
  47    eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.
  48
  49