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.