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 set "baseuri" "cic:/matita/test/russell/".
17 include "nat/orders.ma".
18 include "list/list.ma".
19 include "datatypes/constructors.ma".
21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
22 sig_intro: ∀a:A. P a → sigma A P.
24 interpretation "sigma" 'exists \eta.x =
25 (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x).
27 definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
29 coercion cic:/matita/test/russell/inject.con 0 1.
31 definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
33 coercion cic:/matita/test/russell/eject.con.
35 alias symbol "exists" (instance 2) = "exists".
36 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
38 (λl:list nat. λH:l ≠ [].match l with [ nil ⇒ λH.[] | cons x l1 ⇒ λH.l1] H);
39 letin program_spec ≝ (program : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l);
40 [ generalize in match H; cases l; [intros (h1); cases (h1 ?); reflexivity]
41 intros; apply (ex_intro ? ? n); apply eq_f; reflexivity; ]
45 alias symbol "exists" (instance 3) = "exists".
46 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
48 (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
50 (program : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
51 [ autobatch; | generalize in match H; clear H; cases s; simplify;
52 intros; cases (H H1); ]
56 definition nat_return := λn:nat. Some ? n.
58 coercion cic:/matita/test/russell/nat_return.con.
60 definition raise_exn := None nat.
62 definition try_with :=
63 λx,e. match x with [ None => e | Some (x : nat) => x].
65 lemma hd : list nat → option nat :=
66 λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
70 definition bind ≝ λf:nat->nat.λx.
71 match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
73 include "datatypes/bool.ma".
74 include "list/sort.ma".
75 include "nat/compare.ma".
77 definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
79 coercion cic:/matita/test/russell/inject_opt.con 0 1.
81 definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
83 coercion cic:/matita/test/russell/eject_opt.con.
87 ∀l:list nat. sigma ? (λres:option nat.
89 [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
90 | Some x ⇒ mem ? eqb x l = true ∧ p x = true ]).
96 | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ]
101 (program : ∀p:nat → bool.
102 ∀l:list nat. ∃res:option nat.
104 [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false
105 | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]);
107 [ cases (aux l1); clear aux;
108 simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]);
109 generalize in match H2; clear H2;
113 apply (eqb_elim y n);
131 | unfold nat_return; simplify;
137 | unfold raise_exn; simplify;
139 change in H1 with (false = true);