]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/multiple_inheritance.ma
makefile reworked to make debian package possible
[helm.git] / helm / software / matita / tests / multiple_inheritance.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 set "baseuri" "cic:/matita/test/".
16
17 include "logic/equality.ma".
18
19 record R1 : Type := { C:> Type; plus: C \to C \to C}.
20 record R2 : Type := { K:> Type; mult: K \to K \to K}.
21
22 (* Missing syntactic sugar:
23    record R : Type := { r1 :> R1; r2 :> R2 with C r1 = K r2}
24 *)
25 record R : Type := { r1 :> R1; r2_ : R2; with_: C r1 = K r2_ }.
26
27 (* This can be done automatically *)
28 lemma r2 : R → R2.
29  intro;
30  apply mk_R2;
31  [ apply (C r)
32  | apply (eq_rect ? ? (λx.x → x → x));
33    [3: symmetry;
34        [2: apply (with_ r)
35        | skip
36        ]
37    | skip
38    | apply (mult (r2_ r))
39    ]
40  ].
41 qed.
42 coercion cic:/matita/test/r2.con.
43
44 (* Let's play with it *)
45 definition f ≝ λr:R.λx:r.plus ? (mult ? x x) x.
46
47 axiom plus_idempotent: ∀r1:R1.∀x:r1. plus ? x x = x.
48 axiom mult_idempotent: ∀r2:R2.∀x:r2. mult ? x x = x.
49
50 lemma test: ∀r:R. ∀x:r. f ? x = x.
51  intros;
52  unfold f;
53  auto paramodulation.
54 qed.