]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/coercions_russell.ma
splitting files
[helm.git] / matita / 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
16
17 include "nat/orders.ma".
18 include "list/list.ma".
19 include "datatypes/constructors.ma".
20
21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
22  sig_intro: ∀a:A. P a → sigma A P.
23
24 interpretation "sigma" 'exists \eta.x =
25   (cic:/matita/tests/coercions_russell/sigma.ind#xpointer(1/1) _ x).
26  
27 definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
28
29 coercion cic:/matita/tests/coercions_russell/inject.con 0 1.
30
31 definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
32
33 coercion cic:/matita/tests/coercions_russell/eject.con.
34   
35 alias symbol "exists" (instance 2) = "exists".
36 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
37  apply rule (λl:list nat. λ_.match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
38   [ exists; [2: reflexivity | skip]
39   | destruct; elim H; reflexivity]
40 qed.
41
42 alias symbol "exists" (instance 3) = "exists".
43 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
44 apply rule (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
45 [ autobatch; 
46 | cases s in H; simplify; intros; cases (H H1); ]
47 qed.
48
49 definition nat_return := λn:nat. Some ? n.
50
51 coercion cic:/matita/tests/coercions_russell/nat_return.con.
52
53 definition raise_exn := None nat.
54
55 definition try_with :=
56  λx,e. match x with [ None => e | Some (x : nat) => x].
57
58 lemma hd : list nat → option nat :=
59   λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
60   
61 axiom f : nat -> nat.
62
63 definition bind ≝ λf:nat->nat.λx.
64   match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
65
66 include "datatypes/bool.ma".
67 include "list/sort.ma".
68 include "nat/compare.ma".
69
70 definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
71
72 coercion cic:/matita/tests/coercions_russell/inject_opt.con 0 1.
73
74 definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
75
76 coercion cic:/matita/tests/coercions_russell/eject_opt.con.
77
78 (* we may define mem as in the following lemma and get rid of it *)
79 definition find_spec ≝
80   λl,p.λres:option nat.
81    match res with
82     [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
83     | Some x ⇒ mem ? eqb x l = true ∧ 
84                p x = true ∧ 
85                ∀y.mem ? eqb y l = true → p y = true → x ≠ y → 
86                     ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3].
87
88 lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2.
89 intros 2; elim l (H hd tl IH H); [simplify in H; destruct H]
90 generalize in match H; clear H;
91 simplify; apply (eqb_elim x hd); simplify; intros;
92 [1:clear IH; rewrite < H; apply (ex_intro ? ? []); 
93 |2:lapply(IH H1); clear H1 IH; decompose; rewrite > H2; clear H2]
94 simplify; autobatch;
95 qed.
96
97 notation > "'If' b 'Then' t 'Else' f" non associative
98 with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
99
100 alias symbol "exists" = "sigma".
101 definition sigma_find_spec : ∀p,l. ∃res.find_spec l p res.
102 apply rule (λp. 
103   let rec aux l ≝
104     match l with
105     [ nil ⇒ raise_exn
106     | cons x l ⇒ If p x Then nat_return x Else aux l]
107     in aux);
108 (* l = x::tl ∧ p x = false *)
109 [1: cases (aux l1); clear aux;
110     cases a in H2; simplify;
111     [1: intros 2; apply (eqb_elim y n); intros (Eyn); autobatch;
112     |2: intros; decompose; repeat split; [2: assumption]; intros;
113         [1: cases (eqb n1 n); simplify; autobatch;
114         |2: generalize in match (refl_eq ? (eqb y n));
115             generalize in ⊢ (? ? ? %→?); 
116             intro; cases b; clear b; intro Eyn; rewrite > Eyn in H3; simplify in H3;
117             [1: rewrite > (eqb_true_to_eq ? ? Eyn) in H6; rewrite > H1 in H6; destruct H6;
118             |2: lapply H4; try assumption; decompose; clear H4; rewrite > H8;
119                 simplify; autobatch depth = 4;]]]
120 (* l = x::tl ∧ p x = true *)
121 |2: unfold find_spec; unfold nat_return; simplify; repeat split; [2: assumption]
122     [1: rewrite > eqb_n_n; reflexivity
123     |2: intro; generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
124         intro; cases b; clear b; intro Eyn; rewrite > Eyn; 
125         [1: rewrite > (eqb_true_to_eq ? ? Eyn);] clear Eyn; simplify; intros;
126           [1: cases H4; reflexivity
127           |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
128               apply (ex_intro ? ? []); simplify; autobatch;]]
129 (* l = [] *)
130 |3: unfold raise_exn; simplify; intros; destruct H1;]
131 qed.