goedel.v

From Coq.Bool Require Export Bool.
From Coq.micromega Require Export Lia.
From Coq.Lists Require Export List.
From Coq.Arith Require Export PeanoNat.
From Coq.Strings Require Export String.

Module Goedel's_Incompleteness_Theorem.

Import ListNotations.

Section Preliminaries.

Lemma div_mod_uniqueness :
  forall a : nat,
  forall b : nat,
  forall q : nat,
  forall r : nat,
  a = b * q + r ->
  r < b ->
  a / b = q /\ a mod b = r.
Proof.
  assert (forall x : nat, forall y : nat, x > y <-> (exists z : nat, x = S (y + z))).
  { intros x y; constructor.
    - intros H; induction H.
      + exists 0; lia.
      + destruct IHle as [z H0]; exists (S z); lia.
    - intros H; destruct H as [z H]; lia.
  }
  intros a b q r H1 H2.
  assert (H0 : a = b * (a / b) + (a mod b)) by (apply (Nat.div_mod a b); lia).
  assert (H3 : 0 <= a mod b < b).
  { apply (Nat.mod_bound_pos a b).
    - lia.
    - lia.
  }
  assert (H4 : ~ q > a / b).
  { intros H4.
    assert (H5 : exists z : nat, q = S (a / b + z)) by (apply (H q (a / b)); lia).
    destruct H5 as [z H5].
    cut (b * q + r >= b * S (a / b) + r); lia.
  }
  assert (H5 : ~ q < a / b).
  { intros H5.
    assert (H6 : exists z : nat, a / b = S (q + z)) by (apply (H (a / b) q); lia).
    destruct H6 as [z H6].
    cut (b * q + a mod b >= b * S (a / b) + a mod b); lia.
  }
  assert (H6 : q = a / b) by lia; assert (H7 : r = a mod b) by lia; lia.
Qed.

Fixpoint first_nat (p : nat -> bool) (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => if p (first_nat p n') then first_nat p n' else n
  end
.

Theorem well_ordering_principle : 
  forall p : nat -> bool,
  forall n : nat,
  p n = true ->
  let m := first_nat p n in
  p m = true /\ (forall i : nat, p i = true -> i >= m).
Proof with eauto.
  intros p n H3 m.
  assert (forall x : nat, p x = true -> p (first_nat p x) = true).
  {
    induction x...
    simpl.
    destruct (p (first_nat p x)) eqn:H0...
  }
  constructor...
  intros i H4.
  enough (forall x : nat, first_nat p x <= x).
  enough (forall x : nat, p (first_nat p x) = true -> (forall y : nat, x < y -> first_nat p x = first_nat p y)).
  enough (forall x : nat, forall y : nat, p y = true -> first_nat p x <= y)...
  - intros x y H2.
    destruct (Compare_dec.le_lt_dec x y).
    + eapply Nat.le_trans...
    + replace (first_nat p x) with (first_nat p y)...
  - intros x H1 y H2.
    induction H2; simpl.
    + rewrite H1...
    + rewrite <- IHle.
      rewrite H1...
  - induction x...
    simpl.
    destruct (p (first_nat p x)) eqn:H0...
Qed.

Fixpoint sum_from_0_to (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => n + sum_from_0_to n'
  end
.

Theorem sum_from_0_to_is :
  forall n : nat,
  2 * sum_from_0_to n = n * (S n).
Proof.
  intros n; induction n.
  - intuition.
  - simpl in *; lia.
Qed.

Fixpoint cantor_pairing (n : nat) : nat * nat :=
  match n with
  | 0 => (0, 0)
  | S n' =>
    match cantor_pairing n' with
    | (0, y) => (S y, 0)
    | (S x, y) => (x, S y)
    end
  end
.

Lemma cantor_pairing_is_surjective :
  forall x : nat,
  forall y : nat,
  (x, y) = cantor_pairing (sum_from_0_to (x + y) + y).
Proof.
  cut (forall z : nat, forall y : nat, forall x : nat, z = x + y -> (x, y) = cantor_pairing (sum_from_0_to z + y)); eauto.
  intros z; induction z.
  - intros y x H; assert (H0 : x = 0) by lia; assert (H1 : y = 0) by lia; subst; eauto.
  - intros y; induction y.
    + intros x H.
      assert (H0 : x = S z) by lia.
      subst; simpl cantor_pairing; destruct (cantor_pairing (z + sum_from_0_to z + 0)) eqn: H0.
      assert (H1 : (0, z) = cantor_pairing (sum_from_0_to z + z)) by (apply IHz; reflexivity).
      rewrite Nat.add_0_r in H0; rewrite Nat.add_comm in H0; rewrite H0 in H1.
      inversion H1; subst; reflexivity.
    + intros x H.
      assert (H0 : (S x, y) = cantor_pairing (sum_from_0_to (S z) + y)) by (apply (IHy (S x)); lia).
      assert (H1 : z + sum_from_0_to z + S y = sum_from_0_to (S z) + y) by (simpl; lia).
      simpl; rewrite H1; rewrite <- H0; eauto.
Qed.

Lemma cantor_pairing_is_injective :
  forall n : nat,
  forall x : nat,
  forall y : nat,
  cantor_pairing n = (x, y) ->
  n = sum_from_0_to (x + y) + y.
Proof.
  intros n; induction n.
  - simpl; intros x y H; inversion H; subst; reflexivity.
  - simpl; intros x y H; destruct (cantor_pairing n) as [x' y'] eqn: H0; destruct x'.
    + inversion H; subst; repeat (rewrite Nat.add_0_r); simpl; rewrite (IHn 0 y' eq_refl); rewrite Nat.add_0_l; lia.
    + inversion H; subst; rewrite (IHn (S x) y' eq_refl); assert (H1 : forall x' : nat, S x' + y' = x' + S y') by lia; repeat (rewrite H1); lia.
Qed.

Theorem cantor_pairing_is :
  forall n : nat,
  forall x : nat,
  forall y : nat,
  cantor_pairing n = (x, y) <-> n = sum_from_0_to (x + y) + y.
Proof.
  intros n x y; constructor.
  - apply (cantor_pairing_is_injective n x y).
  - intros H; subst; rewrite (cantor_pairing_is_surjective x y); reflexivity.
Qed.


Inductive FinSet : nat -> Set :=
| FinSetZ :
  forall n : nat,
  FinSet (S n)
| FinSetS :
  forall n : nat,
  FinSet n ->
  FinSet (S n)
.

Fixpoint runFinSet (n : nat) (idx : FinSet n) : {i : nat | i < n} :=
  match idx with
  | FinSetZ i => exist _ i (Le.le_refl _)
  | FinSetS n' idx' =>
    match runFinSet n' idx' with
    | exist _ i H => exist _ i (le_S _ _ H)
    end
  end
.

Example runFinSet_ex1 : runFinSet 2 (FinSetS 1 (FinSetZ 0)) = exist _ 0 (le_S _ _ (Le.le_refl _)) := eq_refl.

Lemma i_lt_0_implies_bang {A : Type} (i : nat) :
  i < 0 ->
  A.
Proof.
  lia.
Qed.

Lemma S_i_lt_S_n_implies_i_lt_n (i : nat) (n : nat) :
  S i < S n ->
  i < n.
Proof.
  lia.
Qed.

Fixpoint makeFinSet (n : nat) : {i : nat | i < n} -> FinSet n :=
  match n as n0 return {i : nat | i < n0} -> FinSet n0 with
  | 0 =>
    fun idx : {i : nat | i < 0} =>
    match idx with
    | exist _ i i_lt_0 => i_lt_0_implies_bang i i_lt_0
    end
  | S n' =>
    fun idx : {i : nat | i < S n'} =>
    match idx with
    | exist _ i i_lt_S_n' =>
      ( match i as i0 return i0 < S n' -> FinSet (S n') with
        | 0 =>
          fun _ : (0 < S n') =>
          FinSetZ n'
        | S i' =>
          fun S_i'_lt_S_n' : (S i' < S n') =>
          FinSetS n' (makeFinSet n' (exist _ i' (S_i_lt_S_n_implies_i_lt_n i' n' S_i'_lt_S_n')))
        end
      ) i_lt_S_n'
    end
  end
.

Example makeFinSet_ex1 : makeFinSet 2 (exist _ 1 (Le.le_refl _)) = FinSetS _ (FinSetZ _) := eq_refl.

Lemma FinSet0_impossible {A : Type} :
  forall n : nat,
  n = 0 ->
  FinSet n ->
  A.
Proof.
  intros n H idx; subst; inversion idx.
Qed.

End Preliminaries.

Section Arithmetic.

Definition arity : Set :=
  nat
.

Inductive Arith : arity -> Set :=
| AVar {ary : arity} : FinSet ary -> Arith ary
| AAdd {ary : arity} : Arith ary -> Arith ary -> Arith ary
| ATms {ary : arity} : Arith ary -> Arith ary -> Arith ary
| A_lt {ary : arity} : Arith ary -> Arith ary -> Arith ary
| A_mu {ary : arity} : Arith (S ary) -> Arith ary
.

Definition w : Set :=
  nat
.

Fixpoint lift (ary : arity) (A : Type) : Type :=
  match ary with
  | 0 => A
  | S ary' => w -> lift ary' A
  end
.

Fixpoint unliftProp (ary : arity) : lift ary Prop -> Prop :=
  match ary with
  | 0 =>
    fun P : Prop =>
    P
  | S ary' =>
    fun A : w -> lift ary' Prop =>
    forall n : w, unliftProp ary' (A n)
  end
.

Fixpoint lift_pure {A : Type} (ary : arity) : A -> lift ary A :=
  match ary with
  | 0 =>
    fun x : A =>
    x
  | S ary' =>
    fun x : A =>
    fun _ : w =>
    lift_pure ary' x
  end
.

Fixpoint lift_ap {A : Type} {B : Type} (ary : arity) : lift ary (A -> B) -> lift ary A -> lift ary B :=
  match ary with
  | 0 =>
    fun f : A -> B =>
    fun x : A =>
    f x
  | S ary' =>
    fun f : w -> lift ary' (A -> B) =>
    fun x : w -> lift ary' A =>
    fun n : w =>
    lift_ap ary' (f n) (x n)
  end
.

Fixpoint lift_assoc {A : Type} (ary : arity) : lift (S ary) A -> lift ary (w -> A) :=
  match ary with
  | 0 =>
    fun x : w -> A =>
    x
  | S ary' =>
    fun x : w -> lift (S ary') A =>
    fun n : w =>
    lift_assoc ary' (x n)
  end
.

Fixpoint lift_bind {A : Type} {B : Type} (ary : arity) : lift ary A -> (A -> lift ary B) -> lift ary B :=
  match ary with
  | 0 =>
    fun x : A =>
    fun f : A -> B =>
    f x
  | S ary' =>
    fun x : w -> lift ary' A =>
    fun f : A -> w -> lift ary' B =>
    fun n : w =>
    lift_bind ary' (x n) (fun a : A => f a n)
  end
.

Fixpoint projection_zero (ary : arity) (val : w) : lift ary w :=
  match ary with
  | 0 =>
    val
  | S ary' =>
    fun _ : w =>
    projection_zero ary' val
  end
.

Fixpoint projection (ary : nat) (idx : FinSet ary) : lift ary w :=
  match idx in FinSet n return lift n w with
  | FinSetZ n' => projection_zero n'
  | FinSetS n' idx' =>
    fun _ : w =>
    projection n' idx'
  end
.

Fixpoint unlift_type (ary : arity) : lift ary Set -> Set :=
  match ary with
  | 0 =>
    fun A : Set =>
    A
  | S ary' =>
    fun A : w -> lift ary' Set =>
    forall n : w, unlift_type ary' (A n)
  end
.

Inductive evalArith : forall ary : arity, Arith ary -> lift ary w -> Prop :=
| evalAVar {ary : arity} :
  forall idx : FinSet ary,
  evalArith ary (AVar idx) (projection ary idx)
| evalAAdd {ary : arity} :
  forall f : lift ary w,
  forall g : lift ary w,
  forall e1 : Arith ary,
  forall e2 : Arith ary,
  evalArith ary e1 f ->
  evalArith ary e2 g ->
  evalArith ary (AAdd e1 e2) (lift_ap ary (lift_ap ary (lift_pure ary plus) f) g)
| evalATms {ary : arity} :
  forall f : lift ary w,
  forall g : lift ary w,
  forall e1 : Arith ary,
  forall e2 : Arith ary,
  evalArith ary e1 f ->
  evalArith ary e2 g ->
  evalArith ary (ATms e1 e2) (lift_ap ary (lift_ap ary (lift_pure ary mult) f) g)
| evalA_lt {ary : arity} :
  forall f : lift ary w,
  forall g : lift ary w,
  forall e1 : Arith ary,
  forall e2 : Arith ary,
  evalArith ary e1 f ->
  evalArith ary e2 g ->
  evalArith ary (A_lt e1 e2) (lift_ap ary (lift_ap ary (lift_pure ary (fun x : w => fun y : w => if Compare_dec.lt_dec x y then 0 else 1)) f) g)
| evalA_mu {ary : arity} :
  forall f : lift (S ary) w,
  forall g : lift ary w,
  forall e1 : Arith (S ary),
  evalArith (S ary) e1 f ->
  let check : lift ary (w -> bool) := lift_ap ary (lift_pure ary (fun f' : w -> w => fun n : w => Nat.eqb (f' n) 0)) (lift_assoc ary f) in
  unliftProp ary (lift_ap ary (lift_ap ary (lift_pure ary (fun x : w => fun f : w -> bool => f x = true)) g) check) ->
  evalArith ary (A_mu e1) (lift_ap ary (lift_ap ary (lift_pure ary first_nat) check) g)
.

Definition IsArithmetic {ary : arity} (func : lift ary w) : Prop :=
  exists e : Arith ary, evalArith ary e func
.

Definition funcIsRecursive {ary : arity} (func : lift ary w) : Prop :=
  exists func1 : lift ary w, IsArithmetic func1 /\ unliftProp ary (lift_ap ary (lift_ap ary (lift_pure ary (fun x : w => fun y : w => x = y)) func) func1)
.

Definition relIsRecursive {ary : arity} (rel : lift ary Prop) : Prop :=
  exists func : lift ary w, funcIsRecursive func /\ unliftProp ary (lift_ap ary (lift_ap ary (lift_pure ary (fun P : Prop => fun n : w => (P -> n = 0) /\ (~ P -> n = 1))) rel) func)
.

Definition IsRecursivelyEnumerable {ary : arity} (rel : lift ary Prop) : Prop :=
  exists rel1 : lift (S ary) Prop, unliftProp ary (lift_ap ary (lift_ap ary (lift_pure ary (fun P : Prop => fun Q : w -> Prop => P <-> exists x : w, Q x)) rel) (lift_assoc ary rel1)) /\ relIsRecursive rel1
.

End Arithmetic.

End Goedel's_Incompleteness_Theorem.