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 set "baseuri" "cic:/matita/demo/realisability/".
  16
  17 include "logic/connectives.ma".
  18 include "datatypes/constructors.ma".
  19
  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
  23
  24    The original Agda file realisability.agda can be found at
  25
  26    http://www.math.uu.se/~palmgren/modif/realisability.agda
  27 *)
  28
  29 inductive SP : Type ≝
  30    abs: SP
  31  | atom: ∀P:Prop.SP
  32  | sand: SP → SP → SP
  33  | sor: SP → SP → SP
  34  | simp: SP → SP → SP
  35  | forall: ∀A:Type. (A → SP) → SP
  36  | exist: ∀A:Type. (A → SP) → SP.
  37
  38 let rec Prop_OF_SP F ≝
  39  match F with
  40   [ abs ⇒ False
  41   | atom P ⇒ P
  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)
  47   ].
  48
  49 inductive sigma (A:Type) (P:A → Type) : Type ≝
  50  sigma_intro: ∀x:A. P x → sigma A P.
  51
  52 definition pi1 ≝
  53  λA,P.λs:sigma A P.
  54   match s with
  55    [ sigma_intro a _ ⇒ a].
  56
  57 definition pi2 ≝
  58  λA,P.λs:sigma A P.
  59   match s return λs.P (pi1 ? ? s) with
  60    [ sigma_intro _ p ⇒ p].
  61
  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}}}.
  67
  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).
  71
  72 let rec type_OF_SP F ≝
  73  match F return λF.Type with
  74   [ abs ⇒ unit
  75   | atom P ⇒ unit
  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)
  81   ].
  82
  83 let rec modr F : type_OF_SP F → Prop ≝
  84  match F return λF.type_OF_SP F → Prop with
  85   [ abs ⇒ λr.False
  86   | atom P ⇒ λr.P
  87   | sand A B ⇒ λr.modr A (\fst r) ∧ modr B (\snd r)
  88   | sor A B ⇒
  89      λr.
  90       match r with
  91        [ inl a ⇒ modr A a
  92        | inr b ⇒ modr B b
  93        ]
  94   | simp A B ⇒
  95      λr.
  96       (Prop_OF_SP A → Prop_OF_SP B) ∧
  97       ∀a:type_OF_SP A. modr A a → modr B (r a)
  98   | forall A F ⇒
  99      λr:Πx:A.type_OF_SP (F x).∀a:A. modr (F a) (r a)
 100   | exist A F ⇒
 101      λr.
 102       modr (F (pi1 ? ? r)) (pi2 ? ? r)
 103   ].
 104
 105 theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F.
 106  intro;
 107  elim F; simplify;
 108   [1,2: apply H
 109   | split; simplify in r H2;
 110      [apply H;
 111        [ apply (\fst r)
 112        | apply (proj1 ? ? H2)
 113        ]
 114      | apply H1;simplify in r H2;
 115        [ apply (\snd r)
 116        | apply (proj2 ? ? H2)
 117        ]
 118      ]
 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
 124      ]
 125   | simplify in H2;
 126     apply (proj1 ? ? H2)
 127   | simplify in H1;
 128     intro;
 129     apply H;
 130     [2: apply H1
 131     | skip
 132     ]
 133   | simplify in r;
 134     generalize in match H1; clear H1;
 135     elim r;
 136     apply (ex_intro ? ? a);
 137     apply H;
 138     assumption
 139   ]
 140 qed.
 141
 142 definition realized ≝
 143  λF:SP.∃r:type_OF_SP F.modr F r.
 144
 145 theorem correct2: ∀F:SP. realized F → Prop_OF_SP F.
 146  intros;
 147  elim H;
 148  apply correct;
 149  assumption.
 150 qed.
 151
 152 theorem extraction:
 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).
 156  intros;
 157  apply (correct2 (exist ? (λb:B. P a b)));
 158  simplify in H; elim H; clear H;
 159  simplify;
 160  apply (ex_intro ? ? (a1 a));
 161  apply H1.
 162 qed.
 163
 164 lemma true_impl_realized:
 165  ∀A,B:Prop. (A → B) → realized (simp (atom A) (atom B)).
 166  intros;
 167  simplify;
 168  apply (ex_intro ? ? (λu.u));
 169  split;
 170   [ assumption
 171   | intro; assumption
 172   ]
 173 qed.
 174
 175 (******** rules for first order logic **********************)
 176
 177 lemma elim_abs: ∀P:Prop. realized (simp abs (atom P)).
 178  intro;
 179  simplify;
 180  apply (ex_intro ? ? (λu.u));
 181  split;
 182   [ intro; cases H
 183   | intros; cases H
 184   ]
 185 qed.
 186
 187 lemma id_axiom: ∀F:SP. realized (simp F F).
 188  intros;
 189  simplify;
 190  apply (ex_intro ? ? (λu.u));
 191  split;
 192   [ intro; assumption
 193   | intros; assumption
 194   ]
 195 qed.
 196
 197 lemma cut:
 198  ∀F1,F2,F3:SP.
 199   realized (simp F1 F2) → realized (simp F2 F3) → realized (simp F1 F3).
 200  intros;
 201  elim H; clear H;
 202  elim H1; clear H1;
 203  simplify in a a1;
 204  apply (ex_intro ? ? (λx.a1 (a x)));
 205  simplify;
 206  simplify in H2 H;
 207  elim H2; clear H2;
 208  elim H; clear H;
 209  split;
 210   [ intro; apply (H2 (H1 H))
 211   | intros; apply (H4 ? (H3 ? H))
 212   ]
 213 qed.
 214
 215 lemma and_i:
 216  ∀F1,F2,F3:SP.
 217   realized (simp F1 F2) → realized (simp F1 F3) → realized (simp F1 (sand F2 F3)).
 218  intros;
 219  elim H; clear H;
 220  elim H1; clear H1;
 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;
 225  split;
 226   [ intro; split; [ apply (H1 H) | apply (H2 H) ]
 227   | intros;
 228     split;
 229      [ simplify; apply H3; assumption
 230      | simplify; apply H4; assumption
 231      ]
 232   ]
 233 qed.
 234
 235 (* Many more rules and examples missing, but trivial. *)