1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/demo/realisability/".
17 include "logic/connectives.ma".
18 include "datatypes/constructors.ma".
20 (* The following is a stranslation in Matita of the initial part of
21 Erik Palmgren, ``Internalizing Modified Realizability in Constructive Type
22 Theory'', Logical Methods in Computer Science, Vol 1 (2:2), 2005, pp. 1--7
24 The original Agda file realisability.agda can be found at
26 http://www.math.uu.se/~palmgren/modif/realisability.agda
35 | forall: ∀A:Type. (A → SP) → SP
36 | exist: ∀A:Type. (A → SP) → SP.
38 let rec Prop_OF_SP F ≝
42 | sand A B ⇒ Prop_OF_SP A ∧ Prop_OF_SP B
43 | sor A B ⇒ Prop_OF_SP A ∨ Prop_OF_SP B
44 | simp A B ⇒ Prop_OF_SP A → Prop_OF_SP B
45 | forall A F ⇒ ∀x:A.Prop_OF_SP (F x)
46 | exist A F ⇒ ∃x:A.Prop_OF_SP (F x)
49 inductive sigma (A:Type) (P:A → Type) : Type ≝
50 sigma_intro: ∀x:A. P x → sigma A P.
55 [ sigma_intro a _ ⇒ a].
59 match s return λs.P (pi1 ? ? s) with
60 [ sigma_intro _ p ⇒ p].
62 notation "hvbox(Σ ident i opt (: ty) break . p)"
63 right associative with precedence 20
64 for @{ 'sigma ${default
65 @{\lambda ${ident i} : $ty. $p}
66 @{\lambda ${ident i} . $p}}}.
68 (*CSC: the URI must disappear: there is a bug now *)
69 interpretation "Sigma" 'sigma \eta.x =
70 (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ x).
72 let rec type_OF_SP F ≝
73 match F return λF.Type with
76 | sand A B ⇒ (type_OF_SP A) × (type_OF_SP B)
77 | sor A B ⇒ type_OF_SP A + type_OF_SP B
78 | simp A B ⇒ type_OF_SP A → type_OF_SP B
79 | forall A F ⇒ Πx:A.type_OF_SP (F x)
80 | exist A F ⇒ Σx:A.type_OF_SP (F x)
83 let rec modr F : type_OF_SP F → Prop ≝
84 match F return λF.type_OF_SP F → Prop with
87 | sand A B ⇒ λr.modr A (\fst r) ∧ modr B (\snd r)
96 (Prop_OF_SP A → Prop_OF_SP B) ∧
97 ∀a:type_OF_SP A. modr A a → modr B (r a)
99 λr:Πx:A.type_OF_SP (F x).∀a:A. modr (F a) (r a)
102 modr (F (pi1 ? ? r)) (pi2 ? ? r)
105 theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F.
112 | apply (proj1 ? ? H2)
116 | apply (proj2 ? ? H2)
119 | generalize in match H2; clear H2;
120 change in r with (type_OF_SP s + type_OF_SP s1);
121 elim r; simplify in H2;
122 [ left; apply H; assumption
123 | right; apply H1; assumption
134 generalize in match H1; clear H1;
136 apply (ex_intro ? ? a);
142 definition realized ≝
143 λF:SP.∃r:type_OF_SP F.modr F r.
145 theorem correct2: ∀F:SP. realized F → Prop_OF_SP F.
153 ∀A,B:Type.∀P: A → B → SP.
154 realized (forall A (λa:A. exist B (λb:B. P a b))) →
155 ∀a:A.∃b:B.Prop_OF_SP (P a b).
157 apply (correct2 (exist ? (λb:B. P a b)));
158 simplify in H; elim H; clear H;
160 apply (ex_intro ? ? (a1 a));
164 lemma true_impl_realized:
165 ∀A,B:Prop. (A → B) → realized (simp (atom A) (atom B)).
168 apply (ex_intro ? ? (λu.u));
175 (******** rules for first order logic **********************)
177 lemma elim_abs: ∀P:Prop. realized (simp abs (atom P)).
180 apply (ex_intro ? ? (λu.u));
187 lemma id_axiom: ∀F:SP. realized (simp F F).
190 apply (ex_intro ? ? (λu.u));
199 realized (simp F1 F2) → realized (simp F2 F3) → realized (simp F1 F3).
204 apply (ex_intro ? ? (λx.a1 (a x)));
210 [ intro; apply (H2 (H1 H))
211 | intros; apply (H4 ? (H3 ? H))
217 realized (simp F1 F2) → realized (simp F1 F3) → realized (simp F1 (sand F2 F3)).
221 simplify in a a1 ⊢ %;
222 apply (ex_intro ? ? (λu.〈a u, a1 u〉));
223 simplify in H2; cases H2; clear H2;
224 simplify in H; cases H; clear H;
226 [ intro; split; [ apply (H1 H) | apply (H2 H) ]
229 [ simplify; apply H3; assumption
230 | simplify; apply H4; assumption
235 (* Many more rules and examples missing, but trivial. *)