matita/tests/coercions_russell.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/russell/".
  16
  17 include "nat/orders.ma".
  18 include "list/list.ma".
  19
  20 inductive sigma (A:Type) (P:A → Prop) : Type ≝
  21  sig_intro: ∀a:A. P a → sigma A P.
  22
  23 interpretation "sigma" 'exists \eta.x =
  24   (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x).
  25
  26 definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
  27
  28 coercion cic:/matita/test/russell/inject.con 0 1.
  29
  30 definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
  31
  32 coercion cic:/matita/test/russell/eject.con.
  33
  34 alias symbol "exists" (instance 2) = "exists".
  35 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
  36 letin program ≝
  37   (λl:list nat. λH:l ≠ [].match l with [ nil ⇒ λH.[] | cons x l1 ⇒ λH.l1] H);
  38 letin program_spec ≝ (program : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l);
  39  [ generalize in match H; cases l; [intros (h1); cases (h1 ?); reflexivity]
  40    intros; apply (ex_intro ? ? n); apply eq_f; reflexivity; ]
  41 exact program_spec;
  42 qed.
  43
  44 alias symbol "exists" (instance 3) = "exists".
  45 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
  46 letin program ≝
  47   (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
  48 letin program_spec ≝
  49   (program : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
  50   [ autobatch; | generalize in match H; clear H; cases s; simplify;
  51     intros; cases (H H1); ]
  52 exact program_spec.
  53 qed.