helm/software/matita/nlibrary/Plogic/russell_support.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 include "Plogic/jmeq.ma".
  16 include "logic/connectives.ma".
  17 include "datatypes/sums.ma".
  18
  19 include "Plogic/connectives.ma".
  20
  21 (* experimental: Russell support *)
  22
  23 alias id "False" = "cic:/matita/ng/Plogic/connectives/False.ind(1,0,0)".
  24
  25 ndefinition P_to_P_option : ∀A:Type[0].∀P:A → CProp[0].option A → CProp[0] ≝
  26   λA,P,a.match a with [ None ⇒ False | Some y ⇒ P y ].
  27
  28 ndefinition subset : ∀A:Type[0].(A → CProp[0]) → Type[0] ≝
  29   λA,P.Σx.P_to_P_option A P x.
  30
  31 notation < "hvbox({ ident i : s | term 19 p })" with precedence 90
  32 for @{ 'subset_spec $s (\lambda ${ident i} : $nonexistent . $p)}.
  33
  34 notation > "hvbox({ ident i : s | term 19 p })" with precedence 90
  35 for @{ 'subset_spec $s (\lambda ${ident i}. $p)}.
  36
  37 (*
  38  * the advantage is that we can use None to mean that some branch of the
  39  * function we are defining will never be reached
  40  * for all other purposes, they are the same as sigma types
  41  *
  42  * TODO: add on-the-fly rewriting for dependent types
  43  *)
  44 interpretation "russell-style subset specification" 'subset_spec s p = (subset s p).
  45
  46 ndefinition inject : ∀A.∀P:A → CProp[0].∀a.∀p:P_to_P_option ? P a.{ x : A | P x } ≝
  47   λA.λP:A → CProp[0].λa:option A.λp:P_to_P_option ? P a.
  48   sig_intro (option A) (P_to_P_option A P) a p.
  49 ndefinition eject : ∀A.∀P: A → CProp[0].{ x : A | P x } → A ≝
  50   λA,P,c.match c with [ sig_intro w p ⇒ ?].
  51 ngeneralize in match p;ncases w;nnormalize
  52 ##[*
  53 ##|#x;#_;napply x ##]
  54 nqed.
  55
  56 ncoercion inject :
  57   ∀A.∀P:A → CProp[0].∀a.∀p:P_to_P_option ? P a.subset ? (λx.P x) ≝ inject
  58   on a:option ? to subset ? ?.
  59 ncoercion eject : ∀A.∀P:A → CProp[0].∀c:subset ? P.A ≝ eject
  60   on _c:subset ? ? to ?.
  61
  62 (*
  63 (* tests...*)
  64
  65 include "datatypes/list.ma".
  66
  67 ndefinition head : ∀l.l ≠ [] → { x : nat | ∃l2.l = x::l2 } ≝
  68  λl,p.match l with
  69   [ nil ⇒ None ?
  70   | cons x tl ⇒ Some ? x ].nnormalize;
  71 ##[ncases p;/3/
  72 ##|/2/
  73 ##]
  74 nqed.
  75
  76 ninductive vec : nat → Type[0] ≝
  77 | vnil : vec O
  78 | vcons : ∀n:nat.nat → vec n → vec (S n).
  79
  80 ndefinition vtail :
  81   ∀n.∀v:vec (S n). { w : vec (pred (S n)) | ∃m:nat.v ≃ vcons ? m w } ≝
  82 λn,v.match v with
  83      [ vnil ⇒ None (vec (pred O))
  84      | vcons p hd tl ⇒ Some (vec (pred (S p))) tl ].
  85 nnormalize;ndestruct;/2/;
  86 nqed.*)