1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "datatypes/pairs.ma".
16 include "sets/setoids.ma".
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 ]].
22 interpretation "eq_pair" 'eq_low a b = (eq_pair ?? a b).
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;
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); //.##]
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 (*---------------------------------------------------------------------------*)⊢
43 unification hint 0 ≔ S1,S2,a,b;
45 L ≟ pair (carr S1) (carr S2)
46 (* -------------------------------------------- *) ⊢
47 eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.