TD9 : Système F

Énoncé

EX 1. Connecteurs logiques dans le système ${\cal F}$

1.

\[\bot ≝ ∀X. X\] \[𝜆x_{\bot ⟹ P}. \; x P : \bot ⟹ Ps\]

2.

Extrait d’un exercice du projet Coq, donné par François Thiré :

Definition my_and (A B : Prop) := forall z:Prop, (A -> B -> z) -> z.


Lemma cons_my_and : forall (A B : Prop), A -> B -> my_and A B.
Proof.
  intros A B HA HB.
  unfold my_and.
  intros.
  apply H.
  easy.
  easy.
Qed.

Lemma my_and_proj1 : forall (A B : Prop), my_and A B -> A.
Proof.
  intros A B H.
  unfold my_and in H.
  apply H; easy.
Qed.

La commande vernaculaire Print donne :

cons_my_and =
fun (A B : Prop) (HA : A) (HB : B) (z : Prop) (H : A -> B -> z) => H HA HB
     : forall A B : Prop, A -> B -> my_and A B

my_and_proj1 =
fun (A B : Prop) (H : my_and A B) => H A (fun (H0 : A) (_ : B) => H0)
    : forall A B : Prop, my_and A B -> A
\[⟨u, v⟩ ≝ 𝜆X. 𝜆f. f \, u \, v \\ 𝜋_1(u_{A_1 ∧ A_2}) ≝ u \; A_1 \; \mathbf{True} \\ 𝜋_2(u_{A_1 ∧ A_2}) ≝ u \; A_2 \; \mathbf{False}\]

3.

Definition my_or2 (A B : Prop) : Prop := forall x:Prop, (A -> x) -> (B -> x) -> x.

Lemma equiv_or : forall (A B : Prop), A \/ B <-> my_or2 A B.
Proof.
  split.
  unfold my_or2.
  intros.
  destruct H.
  apply H0; easy.
  apply H1; easy.
  unfold my_or2.
  intros.
  apply H with (x:=A\/B).
  intros; left; easy.
  intros; right; easy.
Qed.

Print my_or2.

conj
  (fun (H : A \/ B) (x : Prop) (H0 : A -> x) (H1 : B -> x) =>
   match H with
   | or_introl H2 => H0 H2
   | or_intror H2 => H1 H2
   end)
  (fun H : forall x : Prop, (A -> x) -> (B -> x) -> x =>
   H (A \/ B) (fun H0 : A => or_introl H0) (fun H0 : B => or_intror H0))
     : forall A B : Prop, A \/ B <-> my_or2 A B
\[𝜄_i(u) ≝ 𝜆X.𝜆f_1, f_2. f_i u \\ \mathbf{case}(u, x_1 v_1, x_2 v_2) ≝ u C \, (𝜆 x_1. v_1) \, (𝜆 x_2. v_2)\]

4.

\[∃X, F(X) ≝ ¬ ∀X, ¬F(X) = (∀X. F(X) ⟶ \bot) ⟶ \bot\] \[∃X. F(X) ≝ ∀P. (∀X. F(X)⟶P) ⟶ P\] \[⟨⟨T, u_{F(T)}⟩⟩ ≝ 𝜆P. 𝜆Q(P). Q(P) \, T \, u \\ \mathbf{CASE}(u, x.v) ≝ u \, P \, (𝜆X. 𝜆x. v)\]

EX2. Types de données en système ${\cal F}$

1.

$z$ est zéro, $s$ est la fonction successeur.

\[z ≝ 𝜆X. 𝜆x, f. f x\\ s ≝ 𝜆 n. 𝜆X. 𝜆x, f. f (n \, X \, f \, x)\]

2.

\[u : \, ℕ = ∀X. X⟹(X⟹X)⟹X\]

Si $u$ est sous forme normale :

\[u =_𝛽 𝜆X. 𝜆z. 𝜆s. s^n \, z : ∀X. ℕ ⟹ (ℕ ⟹ ℕ) ⟹ ℕ\] \[𝜆X. 𝜆x_X. 𝜆 f_{X⟶X}. f^m (x)\]

pour un certain $m≥0$

3.

\[double ≝ 𝜆n. 𝜆 X. 𝜆x, f. (n X) (n X \, f \, x) f\]

7.

\[incr ≝ 𝜆b. \; 𝜋_2 (b \; ⟨1,2⟩ \; (𝜆⟨b, b'⟩. ⟨i b, ob'⟩) \; (𝜆⟨b, b'⟩. ⟨o b, ib⟩))\]

Leave a comment