1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Plogic/jmeq.ma".
16 include "logic/connectives.ma".
17 include "datatypes/sums.ma".
19 include "Plogic/connectives.ma".
21 (* experimental: Russell support *)
23 alias id "False" = "cic:/matita/ng/Plogic/connectives/False.ind(1,0,0)".
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 ].
28 ndefinition subset : ∀A:Type[0].(A → CProp[0]) → Type[0] ≝
29 λA,P.Σx.P_to_P_option A P x.
31 notation < "hvbox({ ident i : s | term 19 p })" with precedence 90
32 for @{ 'subset_spec $s (\lambda ${ident i} : $nonexistent . $p)}.
34 notation > "hvbox({ ident i : s | term 19 p })" with precedence 90
35 for @{ 'subset_spec $s (\lambda ${ident i}. $p)}.
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
42 * TODO: add on-the-fly rewriting for dependent types
44 interpretation "russell-style subset specification" 'subset_spec s p = (subset s p).
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
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 ?.
65 include "datatypes/list.ma".
67 ndefinition head : ∀l.l ≠ [] → { x : nat | ∃l2.l = x::l2 } ≝
70 | cons x tl ⇒ Some ? x ].nnormalize;
76 ninductive vec : nat → Type[0] ≝
78 | vcons : ∀n:nat.nat → vec n → vec (S n).
81 ∀n.∀v:vec (S n). { w : vec (pred (S n)) | ∃m:nat.v ≃ vcons ? m w } ≝
83 [ vnil ⇒ None (vec (pred O))
84 | vcons p hd tl ⇒ Some (vec (pred (S p))) tl ].
85 nnormalize;ndestruct;/2/;