]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/demo/realisability.ma
d1b569c4075ddc7abf362856eb683840b8e35d74
[helm.git] / helm / software / matita / library / demo / realisability.ma
1 (**************************************************************************)
2 (*       ___                                                                  *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "logic/connectives.ma".
16 include "datatypes/constructors.ma".
17
18 (* The following is a stranslation in Matita of the initial part of
19    Erik Palmgren, ``Internalizing Modified Realizability in Constructive Type
20    Theory'', Logical Methods in Computer Science, Vol 1 (2:2), 2005, pp. 1--7
21    
22    The original Agda file realisability.agda can be found at
23    
24    http://www.math.uu.se/~palmgren/modif/realisability.agda
25 *)
26
27 inductive SP : Type ≝
28    abs: SP
29  | atom: ∀P:Prop.SP
30  | sand: SP → SP → SP
31  | sor: SP → SP → SP
32  | simp: SP → SP → SP
33  | forall: ∀A:Type. (A → SP) → SP
34  | exist: ∀A:Type. (A → SP) → SP.
35
36 let rec Prop_OF_SP F ≝
37  match F with
38   [ abs ⇒ False
39   | atom P ⇒ P
40   | sand A B ⇒ Prop_OF_SP A ∧ Prop_OF_SP B
41   | sor A B ⇒ Prop_OF_SP A ∨ Prop_OF_SP B
42   | simp A B ⇒ Prop_OF_SP A → Prop_OF_SP B
43   | forall A F ⇒ ∀x:A.Prop_OF_SP (F x)
44   | exist A F ⇒ ∃x:A.Prop_OF_SP (F x)
45   ].
46
47 inductive sigma (A:Type) (P:A → Type) : Type ≝
48  sigma_intro: ∀x:A. P x → sigma A P.
49
50 definition pi1 ≝
51  λA,P.λs:sigma A P.
52   match s with
53    [ sigma_intro a _ ⇒ a].
54
55 definition pi2 ≝
56  λA,P.λs:sigma A P.
57   match s return λs.P (pi1 ? ? s) with
58    [ sigma_intro _ p ⇒ p].
59
60 notation "hvbox(\Sigma ident i opt (: ty) break . p)"
61   right associative with precedence 20
62 for @{ 'sigma ${default
63   @{\lambda ${ident i} : $ty. $p}
64   @{\lambda ${ident i} . $p}}}.
65
66 (*CSC: the URI must disappear: there is a bug now *)
67 interpretation "Sigma" 'sigma \eta.x =
68   (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ x).
69
70 let rec type_OF_SP F ≝
71  match F return λF.Type with
72   [ abs ⇒ unit
73   | atom P ⇒ unit
74   | sand A B ⇒ (type_OF_SP A) × (type_OF_SP B)
75   | sor A B ⇒ type_OF_SP A + type_OF_SP B
76   | simp A B ⇒ type_OF_SP A → type_OF_SP B
77   | forall A F ⇒ Πx:A.type_OF_SP (F x)
78   | exist A F ⇒ Σx:A.type_OF_SP (F x)
79   ].
80
81 let rec modr F : type_OF_SP F → Prop ≝
82  match F return λF.type_OF_SP F → Prop with
83   [ abs ⇒ λr.False
84   | atom P ⇒ λr.P
85   | sand A B ⇒ λr.modr A (\fst r) ∧ modr B (\snd r)
86   | sor A B ⇒
87      λr.
88       match r with
89        [ inl a ⇒ modr A a
90        | inr b ⇒ modr B b
91        ]
92   | simp A B ⇒
93      λr.
94       (Prop_OF_SP A → Prop_OF_SP B) ∧
95       ∀a:type_OF_SP A. modr A a → modr B (r a)
96   | forall A F ⇒
97      λr:Πx:A.type_OF_SP (F x).∀a:A. modr (F a) (r a)
98   | exist A F ⇒
99      λr.
100       modr (F (pi1 ? ? r)) (pi2 ? ? r)
101   ].
102
103 theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F.
104  intro;
105  elim F; simplify;
106   [1,2: apply H
107   | split; simplify in r H2; 
108      [apply H;
109        [ apply (\fst r)
110        | apply (proj1 ? ? H2)
111        ]
112      | apply H1;simplify in r H2;
113        [ apply (\snd r)
114        | apply (proj2 ? ? H2)
115        ]
116      ]
117   | change in r with (type_OF_SP s + type_OF_SP s1);
118     elim r in H2 ⊢ %; simplify in H2;
119      [ left; apply H; assumption
120      | right; apply H1; assumption
121      ]
122   | simplify in H2;
123     apply (proj1 ? ? H2)
124   | simplify in H1;
125     intro;
126     apply H;
127     [2: apply H1
128     | skip
129     ]
130   | simplify in r;
131     elim r in H1 ⊢ %;
132     apply (ex_intro ? ? a);
133     apply H;
134     assumption
135   ]
136 qed.
137
138 definition realized ≝
139  λF:SP.∃r:type_OF_SP F.modr F r.
140
141 theorem correct2: ∀F:SP. realized F → Prop_OF_SP F.
142  intros;
143  elim H;
144  apply correct;
145  assumption.
146 qed.
147
148 theorem extraction:
149  ∀A,B:Type.∀P: A → B → SP.
150   realized (forall A (λa:A. exist B (λb:B. P a b))) →
151    ∀a:A.∃b:B.Prop_OF_SP (P a b).
152  intros;
153  apply (correct2 (exist ? (λb:B. P a b)));
154  simplify in H; elim H; clear H;
155  simplify;
156  apply (ex_intro ? ? (a1 a));
157  apply H1.
158 qed.
159
160 lemma true_impl_realized:
161  ∀A,B:Prop. (A → B) → realized (simp (atom A) (atom B)).
162  intros;
163  simplify;
164  apply (ex_intro ? ? (λu.u));
165  split;
166   [ assumption
167   | intro; assumption
168   ]
169 qed.
170
171 (******** rules for first order logic **********************)
172
173 lemma elim_abs: ∀P:Prop. realized (simp abs (atom P)).
174  intro;
175  simplify;
176  apply (ex_intro ? ? (λu.u));
177  split;
178   [ intro; cases H
179   | intros; cases H
180   ]
181 qed.
182
183 lemma id_axiom: ∀F:SP. realized (simp F F).
184  intros;
185  simplify;
186  apply (ex_intro ? ? (λu.u));
187  split;
188   [ intro; assumption
189   | intros; assumption
190   ]
191 qed.
192
193 lemma cut:
194  ∀F1,F2,F3:SP.
195   realized (simp F1 F2) → realized (simp F2 F3) → realized (simp F1 F3).
196  intros;
197  elim H; clear H;
198  elim H1; clear H1;
199  simplify in a a1;
200  apply (ex_intro ? ? (λx.a1 (a x)));
201  simplify;
202  simplify in H2 H;
203  elim H2; clear H2;
204  elim H; clear H;
205  split;
206   [ intro; apply (H2 (H1 H))
207   | intros; apply (H4 ? (H3 ? H))
208   ]
209 qed.
210
211 lemma and_i:
212  ∀F1,F2,F3:SP.
213   realized (simp F1 F2) → realized (simp F1 F3) → realized (simp F1 (sand F2 F3)).
214  intros;
215  elim H; clear H;
216  elim H1; clear H1;
217  simplify in a a1 ⊢ %;
218  apply (ex_intro ? ? (λu.〈a u, a1 u〉));
219  simplify in H2; cases H2; clear H2;
220  simplify in H; cases H; clear H;
221  split;
222   [ intro; split; [ apply (H1 H) | apply (H2 H) ] 
223   | intros;
224     split;
225      [ simplify; apply H3; assumption
226      | simplify; apply H4; assumption
227      ]
228   ]
229 qed.
230
231 (* Many more rules and examples missing, but trivial. *)