]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/multiple_inheritance.ma
restructuring
[helm.git] / matita / 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
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  [ exact (C r)
32  | rewrite > (with_ r); exact (mult (r2_ r))]
33 qed.
34 coercion cic:/matita/tests/multiple_inheritance/r2.con.
35
36 (* convertibility test *)
37 lemma conv_test : ∀r:R.C r -> K r.
38   intros.
39   change with (C (r1 r)).
40   change with (K (r2 r)).
41   change with (C (r1 r)).
42   assumption.
43 qed.
44
45 (* Let's play with it *)
46 definition f ≝ λr:R.λx:r.plus ? (mult ? x x) x.
47
48 axiom plus_idempotent: ∀r1:R1.∀x:r1. plus ? x x = x.
49 axiom mult_idempotent: ∀r2:R2.∀x:r2. mult ? x x = x.
50
51 lemma test: ∀r:R. ∀x:r. f ? x = x.
52  intros;
53  unfold f;
54  autobatch paramodulation.
55 qed.
56
57
58