X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Fdemo%2Frealisability.ma;fp=matita%2Flibrary%2Fdemo%2Frealisability.ma;h=0cd58c63dce78b1c70fe0640541c2d405c73621e;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/demo/realisability.ma b/matita/library/demo/realisability.ma
new file mode 100644
index 000000000..0cd58c63d
--- /dev/null
+++ b/matita/library/demo/realisability.ma
@@ -0,0 +1,235 @@
+(**************************************************************************)
+(*       ___	                                                              *)
+(*      ||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         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/demo/realisability/".
+
+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(Σ ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'sigma ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "Sigma" 'sigma \eta.x =
+  (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ 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)
+       ]
+     ]
+  | generalize in match H2; clear H2;
+    change in r with (type_OF_SP s + type_OF_SP s1);
+    elim r; 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;
+    generalize in match H1; clear H1;
+    elim r;
+    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. *)