(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| A.Asperti, C.Sacerdoti Coen, *) (* ||A|| E.Tassi, S.Zacchiroli *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU Lesser General Public License Version 2.1 *) (* *) (**************************************************************************) include "logic/connectives.ma". include "datatypes/constructors.ma". (* The following is a stranslation in Matita of the initial part of Erik Palmgren, Internalizing Modified Realizability in Constructive Type Theory'', Logical Methods in Computer Science, Vol 1 (2:2), 2005, pp. 1--7 The original Agda file realisability.agda can be found at http://www.math.uu.se/~palmgren/modif/realisability.agda *) inductive SP : Type ≝ abs: SP | atom: ∀P:Prop.SP | sand: SP → SP → SP | sor: SP → SP → SP | simp: SP → SP → SP | forall: ∀A:Type. (A → SP) → SP | exist: ∀A:Type. (A → SP) → SP. let rec Prop_OF_SP F ≝ match F with [ abs ⇒ False | atom P ⇒ P | sand A B ⇒ Prop_OF_SP A ∧ Prop_OF_SP B | sor A B ⇒ Prop_OF_SP A ∨ Prop_OF_SP B | simp A B ⇒ Prop_OF_SP A → Prop_OF_SP B | forall A F ⇒ ∀x:A.Prop_OF_SP (F x) | exist A F ⇒ ∃x:A.Prop_OF_SP (F x) ]. inductive sigma (A:Type) (P:A → Type) : Type ≝ sigma_intro: ∀x:A. P x → sigma A P. definition pi1 ≝ λA,P.λs:sigma A P. match s with [ sigma_intro a _ ⇒ a]. definition pi2 ≝ λA,P.λs:sigma A P. match s return λs.P (pi1 ? ? s) with [ sigma_intro _ p ⇒ p]. notation "hvbox(\Sigma ident i opt (: ty) break . p)" right associative with precedence 20 for @{ 'sigma ${default @{\lambda${ident i} : $ty.$p} @{\lambda ${ident i} .$p}}}. interpretation "Sigma" 'sigma \eta.x = (sigma ? x). let rec type_OF_SP F ≝ match F return λF.Type with [ abs ⇒ unit | atom P ⇒ unit | sand A B ⇒ (type_OF_SP A) × (type_OF_SP B) | sor A B ⇒ type_OF_SP A + type_OF_SP B | simp A B ⇒ type_OF_SP A → type_OF_SP B | forall A F ⇒ Πx:A.type_OF_SP (F x) | exist A F ⇒ Σx:A.type_OF_SP (F x) ]. let rec modr F : type_OF_SP F → Prop ≝ match F return λF.type_OF_SP F → Prop with [ abs ⇒ λr.False | atom P ⇒ λr.P | sand A B ⇒ λr.modr A (\fst r) ∧ modr B (\snd r) | sor A B ⇒ λr. match r with [ inl a ⇒ modr A a | inr b ⇒ modr B b ] | simp A B ⇒ λr. (Prop_OF_SP A → Prop_OF_SP B) ∧ ∀a:type_OF_SP A. modr A a → modr B (r a) | forall A F ⇒ λr:Πx:A.type_OF_SP (F x).∀a:A. modr (F a) (r a) | exist A F ⇒ λr. modr (F (pi1 ? ? r)) (pi2 ? ? r) ]. theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F. intro; elim F; simplify; [1,2: apply H | split; simplify in r H2; [apply H; [ apply (\fst r) | apply (proj1 ? ? H2) ] | apply H1;simplify in r H2; [ apply (\snd r) | apply (proj2 ? ? H2) ] ] | change in r with (type_OF_SP s + type_OF_SP s1); elim r in H2 ⊢ %; simplify in H2; [ left; apply H; assumption | right; apply H1; assumption ] | simplify in H2; apply (proj1 ? ? H2) | simplify in H1; intro; apply H; [2: apply H1 | skip ] | simplify in r; elim r in H1 ⊢ %; apply (ex_intro ? ? a); apply H; assumption ] qed. definition realized ≝ λF:SP.∃r:type_OF_SP F.modr F r. theorem correct2: ∀F:SP. realized F → Prop_OF_SP F. intros; elim H; apply correct; assumption. qed. theorem extraction: ∀A,B:Type.∀P: A → B → SP. realized (forall A (λa:A. exist B (λb:B. P a b))) → ∀a:A.∃b:B.Prop_OF_SP (P a b). intros; apply (correct2 (exist ? (λb:B. P a b))); simplify in H; elim H; clear H; simplify; apply (ex_intro ? ? (a1 a)); apply H1. qed. lemma true_impl_realized: ∀A,B:Prop. (A → B) → realized (simp (atom A) (atom B)). intros; simplify; apply (ex_intro ? ? (λu.u)); split; [ assumption | intro; assumption ] qed. (******** rules for first order logic **********************) lemma elim_abs: ∀P:Prop. realized (simp abs (atom P)). intro; simplify; apply (ex_intro ? ? (λu.u)); split; [ intro; cases H | intros; cases H ] qed. lemma id_axiom: ∀F:SP. realized (simp F F). intros; simplify; apply (ex_intro ? ? (λu.u)); split; [ intro; assumption | intros; assumption ] qed. lemma cut: ∀F1,F2,F3:SP. realized (simp F1 F2) → realized (simp F2 F3) → realized (simp F1 F3). intros; elim H; clear H; elim H1; clear H1; simplify in a a1; apply (ex_intro ? ? (λx.a1 (a x))); simplify; simplify in H2 H; elim H2; clear H2; elim H; clear H; split; [ intro; apply (H2 (H1 H)) | intros; apply (H4 ? (H3 ? H)) ] qed. lemma and_i: ∀F1,F2,F3:SP. realized (simp F1 F2) → realized (simp F1 F3) → realized (simp F1 (sand F2 F3)). intros; elim H; clear H; elim H1; clear H1; simplify in a a1 ⊢ %; apply (ex_intro ? ? (λu.〈a u, a1 u〉)); simplify in H2; cases H2; clear H2; simplify in H; cases H; clear H; split; [ intro; split; [ apply (H1 H) | apply (H2 H) ] | intros; split; [ simplify; apply H3; assumption | simplify; apply H4; assumption ] ] qed. (* Many more rules and examples missing, but trivial. *)