(*
Copyright (c) 2014, Vincent Siles, All rights reserved.

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3.0 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library.
*)

(*
This module started as an exercise to translate Martin Escardo's Agda proof
of omniscient of N\inf into Coq (the link provided at 
http://permalink.gmane.org/gmane.comp.lang.agda/3123
is unfortunately broken now)
.
The translation is quite litteral, with lots of assertions. I should tidy it a
bit someday.

Sorry for the unreadable names of lemmas ;)

V.
*)

Definition N2 := nat -> bool.

(* -- Definition (Natural order of binary numbers) *)
Definition le_bool (a b: bool) := a = true -> b = true. 

Definition ge_bool (a b : bool) := le_bool b a. 

(* -- Definition (Minimum of binary numbers). *)
Definition min (a b: bool) : bool := 
 match a with
   | false => false
   | true => b
 end.

Lemma min_ab_le_a: forall a b, le_bool (min a b) a. 
Proof.
now destruct a; destruct b; intuition.
Qed.

(* -- Definition (Extensional equality on the Cantor space). *)
Definition EqCantor (a b : N2) := forall i, a i = b i.

Definition Inf : N2 := fun _ => true.

(* -- Definition (Extensional ₂-valued functions on the Cantor space). *)
Definition extensional (P: N2 -> bool) := forall (a b : N2), EqCantor a b -> P a = P b.

Lemma extensionality : forall (X Y:Type) (f: X -> Y) (x y: X), x = y -> f x = f y.
Proof.
now intros; subst.
Qed.

Definition Ninf (P: N2) := forall i, ge_bool (P i) (P (S i)).

Fixpoint underline (n:nat) : N2 := 
  match n with
    | O => fun _ => false
    | S p => fun q => match q with 
                         | 0 => true
                         | S r => underline p r
                     end
  end.


Lemma underline0: forall n, underline n n = false.
Proof.
now induction n as [ | n hi]; intuition.
Qed.

Lemma underline1: forall n, underline (S n) n = true.
Proof.
now induction n as [ | n hi]; intuition.
Qed.

Lemma x0_eq_false_impl_x_eqCantor_underline0: forall (x: N2), Ninf x -> x 0  = false -> EqCantor x (underline 0).
Proof.
intros x hinf base n.
induction n as [ | n hi].
- now rewrite base; simpl.
- simpl in *.
  unfold Ninf in hinf.
  specialize hinf with n.
  unfold ge_bool, le_bool in hinf.
  destruct (x n).
  discriminate.
  destruct (x (S n)).
  symmetry; now apply hinf.
  reflexivity.
Qed. 

Definition prd (k : N2) : N2 := fun n => k (S n).

Lemma Ninf_closed_under_prd: forall (x: N2), Ninf x -> Ninf (prd x).
Proof.
intros x hinf n.
unfold ge_bool, prd, le_bool; intros h.
now apply hinf.
Qed.

Lemma xn_eq_true_impl_xSn_eq_false_impl_x_eq_underlineSn:
  forall (x: N2), Ninf x -> forall n, x n = true -> x (S n) = false -> EqCantor x (underline (S n)).
Proof.
intros x hx n; revert x hx.
induction n as [ | n hi]; intros x m r s i.
  assert (by_cases: EqCantor x (underline 1)).
  intros [ | p].
  - simpl in *; assumption.
  - assert (by_nested_induction: forall i, x (S i) = false).
    induction i0 as [ | i0 hi].
    + assumption.
    + unfold Ninf in m; specialize m with (S i0).
      unfold ge_bool, le_bool in m.
      destruct (x (S (S i0))).
      * now rewrite m in hi.
      * reflexivity.
    + now apply by_nested_induction.
  - now apply by_cases.

  - destruct i as [ | i].
    + assert (by_nested_induction : forall n, x n = true -> x 0 = true).
      induction n0 as [ | n0 h1].
      * tauto.
      * unfold Ninf in m; specialize m with n0.
        unfold ge_bool, le_bool in m.
        now intuition.
      * now apply (by_nested_induction (S n)).
     + apply (hi (prd x)).
       now apply Ninf_closed_under_prd.
       now intuition.
       now intuition.
Qed.

Lemma Ninf_underline_N_le_Inf: forall (x: N2), Ninf x-> (forall n, ~ EqCantor x(underline n)) -> 
  EqCantor x Inf.
Proof.
intros x m f.
assert (lemma: forall n, x n = true).
  induction n as [ | n hi].
    assert (claim: x 0 <> false).
      intros r; apply (f 0).
      now apply x0_eq_false_impl_x_eqCantor_underline0.
    now destruct (x 0); intuition.
    assert (claim: x (S n) <> false).
      intros r; apply (f (S n)).
      now apply xn_eq_true_impl_xSn_eq_false_impl_x_eq_underlineSn.
    now destruct (x (S n)); intuition.
now intros r; apply lemma.
Qed.

Lemma density: forall (P: N2 -> bool), extensional P -> (forall n, P (underline n) = true) ->
  P Inf = true -> forall (x: N2), Ninf x -> P x = true.
Proof.
intros p hext f r x m.
assert (claim: forall n, p x = false -> ~ EqCantor x (underline n)).
  intros n hp hc.
  apply hext in hc.
  rewrite (f n) in hc; rewrite hp in hc; discriminate.

assert(claim': p x = false -> forall n, ~EqCantor x (underline n)).
  now intros hp n; apply claim.

assert (claimInf: p x = false -> ~EqCantor x Inf).
  intros hp hc; apply hext in hc.
  rewrite hp in hc; rewrite r in hc; discriminate hc.

assert (lemma: p x <> false).
  intro t.
  apply claimInf.
  assumption.
  now apply (Ninf_underline_N_le_Inf x m (claim' t)).

now destruct (p x); intuition.
Qed.

Fixpoint x (P: N2 -> bool) (n:nat) { struct n } : bool :=
  match n with
    | O => P (underline 0)
    | S n => min (x P n) (P (underline(S n)))
  end.

Theorem T3_6 : forall P: N2 -> bool, extensional P -> {x: N2 & Ninf x /\ 
    (P x = true -> forall y: N2, Ninf y -> P y = true) }.
Proof. 
intros P hext .

assert (lemma0: Ninf (x P)).
  now intros b; apply min_ab_le_a.

assert (dagger0: forall n, EqCantor (x P) (underline n) -> P (underline n) = false).
  destruct n as [ | n].
    intros r.
    now apply (r 0).

    intros r.
    assert (s : x P n = true).
      transitivity (underline (S n) n).
      now apply (r n).
      now apply underline1.

    assert (t : x P (S n) = false).
      transitivity (underline (S n) (S n)).
      now apply (r (S n)).
      now apply underline0.

    assert (u: P (underline (S n)) = x P (S n)).
      now simpl; rewrite s; simpl.

    now rewrite u.

assert (dagger1: EqCantor (x P) Inf -> forall n, P (underline n) = true).
  intros r [ | n ].
  now apply (r 0).

  assert (s: x P n = true) by (apply r).
  assert (t: x P (S n) = true) by apply r.
  assert (u: P (underline (S n)) = x P (S n)).
    now simpl; rewrite s; simpl.

  now rewrite u.

assert (claim0: P (x P) = true -> forall n, ~(EqCantor (x P) (underline n))).
  intros r n s.
  assert (lemma : EqCantor (x P ) (underline n) -> P (x P) = false).
  apply hext in s.
  rewrite s.
  now apply dagger0.

  rewrite r in lemma.
  now discriminate (lemma s).

assert (claim1 : P (x P) = true -> EqCantor (x P) Inf).
  intros r.
  now apply (Ninf_underline_N_le_Inf (x P) lemma0 (claim0 r)).

assert (claim2: P (x P) = true -> forall n, P (underline n) = true).
  intros r.
  now apply (dagger1 (claim1 r)).

assert (claim3: P (x P) = true -> P Inf = true).
  assert (fact: forall a b, a = true -> a = b -> b = true) by (intros; subst; intuition).
  intro r.
  apply (fact _ _ r).
  apply hext.
  now apply (claim1 r).

assert (lemma1: P (x P) = true -> forall (y: N2), Ninf y -> P y = true).
  intro r.
  apply (density P).
  assumption.
  now apply claim2.
  now apply claim3.

now exists (x P); intuition.
Qed.

Lemma two_equality_cases : forall (A: Type) (b: bool), (b = false -> A) -> (b = true -> A) -> A. 
Proof.
intros A b hfalse htrue.
now destruct b; intuition.
Qed.

Theorem Ninf_is_omniscient: forall (p: N2 -> bool), extensional p -> 
   {x: N2 & Ninf x /\ p x = false}+{forall x: N2, Ninf x -> p x = true}.
Proof.
intros p hext.
assert (e: {x : N2 & Ninf x /\ (p x = true -> forall y: N2, Ninf y -> p y = true)}).
  now apply T3_6.

destruct e as [x [m hx2]].

assert (case0: p x = false -> {x0 : N2 & Ninf x0 /\ p x0 = false}+{forall x0: N2, Ninf x0 -> p x0 = true }).
  intros r; left.
  now exists x; split.

assert (case1: p x = true -> {x0 : N2 & Ninf x0 /\ p x0 = false}+{forall x0: N2, Ninf x0 -> p x0 = true }).
  intros r; right.
  intros y hy; now apply hx2.

now apply (two_equality_cases _ (p x)).
Qed.

Print Assumptions Ninf_is_omniscient.