X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2Fmultiple_inheritance.ma;fp=matita%2Ftests%2Fmultiple_inheritance.ma;h=1aa708fb1264bc1be037d2e3f5c8241f44e90b71;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/multiple_inheritance.ma b/matita/tests/multiple_inheritance.ma
new file mode 100644
index 000000000..1aa708fb1
--- /dev/null
+++ b/matita/tests/multiple_inheritance.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+include "logic/equality.ma".
+
+record R1 : Type := { C:> Type; plus: C \to C \to C}.
+record R2 : Type := { K:> Type; mult: K \to K \to K}.
+
+(* Missing syntactic sugar:
+   record R : Type := { r1 :> R1; r2 :> R2 with C r1 = K r2}
+*)
+record R : Type := { r1 :> R1; r2_ : R2; with_: C r1 = K r2_ }.
+
+(* This can be done automatically *)
+lemma r2 : R → R2.
+ intro;
+ apply mk_R2;
+ [ exact (C r)
+ | rewrite > (with_ r); exact (mult (r2_ r))]
+qed.
+coercion cic:/matita/tests/multiple_inheritance/r2.con.
+
+(* convertibility test *)
+lemma conv_test : ∀r:R.C r -> K r.
+  intros.
+  change with (C (r1 r)).
+  change with (K (r2 r)).
+  change with (C (r1 r)).
+  assumption.
+qed.
+
+(* Let's play with it *)
+definition f ≝ λr:R.λx:r.plus ? (mult ? x x) x.
+
+axiom plus_idempotent: ∀r1:R1.∀x:r1. plus ? x x = x.
+axiom mult_idempotent: ∀r2:R2.∀x:r2. mult ? x x = x.
+
+lemma test: ∀r:R. ∀x:r. f ? x = x.
+ intros;
+ unfold f;
+ autobatch paramodulation.
+qed.
+
+
+