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. *)