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