Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.

No title

Require Import Arith.
Require Import Omega.

CoInductive conat :=
| cO : conat
| cS : conat -> conat.

(* A few helper definitions.*)
CoFixpoint inf : conat := cS inf.
Definition unfold_conat (c : conat) : conat :=
  match c with
  | cO => cO
  | cS c => cS c
  end.
Lemma unfold_conat_eq (c : conat) : c = unfold_conat c.
Proof.
  now destruct c.
Qed.

(* Co-inductive equality on conats. *)
CoInductive conat_eq : conat -> conat -> Prop :=
| conat_eq_O : conat_eq cO cO
| conat_eq_S : forall n1 n2, conat_eq n1 n2 -> conat_eq (cS n1) (cS n2).

(* You probably cannot prove this, but it should hold for any specific
   (and constructive) p. *)
Axiom conat_eq_fun : forall (p : conat -> bool) (c d : conat), conat_eq c d -> p c = p d.

(* Comparison of two conats. *)
CoInductive conat_lt (c : conat) : conat -> Prop :=
| conat_lt_c : conat_lt c (cS c)
| conat_lt_S : forall (d : conat), conat_lt c d -> conat_lt c (cS d).

Lemma conat_lt_O_S (c : conat) : conat_lt cO (cS c).
Proof.
  revert c. cofix.
  destruct c.
  - constructor.
  - constructor. apply conat_lt_O_S.
Qed.

(* Injection of nats into conats. *)
Fixpoint add_nat_to_conat (n : nat) (c : conat) : conat :=
  match n with
  | O => c
  | S n => cS (add_nat_to_conat n c)
  end.
Definition nat_to_conat (n : nat) : conat := add_nat_to_conat n cO.

(* Few helper lemmas about it. *)
Lemma add_nat_to_conat_cS (n : nat) (c : conat) :
  add_nat_to_conat n (cS c) = cS (add_nat_to_conat n c).
Proof.
  induction n.
  - reflexivity.
  - simpl. now f_equal.
Qed.

Lemma conat_lt_from_nat (n m : nat) : n < m -> conat_lt (nat_to_conat n) (nat_to_conat m).
Proof.
  induction 1.
  - rewrite (unfold_conat_eq (nat_to_conat (S n))). simpl.
    constructor.
  - rewrite (unfold_conat_eq (nat_to_conat (S m))). simpl.
    now constructor.
Qed.

Lemma add_nat_to_conat_sub_1 (n : nat) (c : conat) : n > 0 ->
  add_nat_to_conat (n - 1) (cS c) = add_nat_to_conat n c.
Proof.
  intros.
  replace n with (S (n - 1)) at 2 by omega.
  simpl. now rewrite add_nat_to_conat_cS.
Qed.

Lemma add_nat_to_conat_sub_1' (n : nat) (c : conat) : n > 0 ->
  add_nat_to_conat n c = cS (add_nat_to_conat (n - 1) c).
Proof.
  intros.
  now replace n with (S (n - 1)) at 1 by omega.
Qed.

(* Finit conats. *)
Definition lt_inf (c : conat) : Prop := exists n, c = nat_to_conat n.
Lemma lt_inf_S (c : conat) : lt_inf c -> lt_inf (cS c).
Proof.
  destruct 1. exists (S x).
  rewrite (unfold_conat_eq (nat_to_conat (S x))). simpl.
  now f_equal.
Qed.

(* Finally, your definition. *)
CoFixpoint root_main (p : conat -> bool) (i : conat) : conat :=
if p i
  then cO
  else cS (root_main p (cS i)).

Definition root (p : conat -> bool) : conat := root_main p cO.

(* Not useful in this case I think, but provable. *)
Lemma root_always_false :
  forall p : conat -> bool,
  (forall c, p c = false) -> conat_eq (root p) inf.
Proof.
  intros.
  unfold root. generalize cO.
  cofix. intros.
  rewrite (unfold_conat_eq (root_main p c)).
  rewrite (unfold_conat_eq inf).
  simpl. rewrite H. constructor.
  apply root_always_false.
Qed.

Lemma root_lt_inf_false :
  forall p : conat -> bool,
  (forall c, lt_inf c -> p c = false) -> conat_eq (root p) inf.
Proof.
  intros.
  unfold root.
  enough (forall (c : conat), lt_inf c -> conat_eq (root_main p c) inf).
  { apply H0. now exists 0. }
  cofix. intros.
  rewrite (unfold_conat_eq (root_main p c)).
  rewrite (unfold_conat_eq inf).
  simpl. rewrite H; [|assumption].
  constructor. apply root_lt_inf_false.
  now apply lt_inf_S.
Qed.

Lemma root_lt_precise :
  forall (p : conat -> bool) (c : conat),
  (lt_inf c /\ p c = true /\ (forall d, conat_lt d c -> p d = false)) -> root p = c.
Proof.
  intros. destruct H as [[n Hcn] [Hc H]].
  enough (forall m, m <= n -> add_nat_to_conat (n - m) (root_main p (nat_to_conat (n - m))) = c).
  { specialize (H0 n (le_n n)). rewrite Nat.sub_diag in H0. apply H0. }
  refine (nat_rect (fun m => m <= n ->
    add_nat_to_conat (n - m) (root_main p (nat_to_conat (n - m))) = c) _ _);
  intros; simpl in *; subst.
  - rewrite Nat.sub_0_r.
    rewrite (unfold_conat_eq (root_main p (nat_to_conat n))). simpl.
    now rewrite Hc.
  - intros.
    rewrite (unfold_conat_eq (root_main p (nat_to_conat (n - S n0)))). simpl.
    assert (p (nat_to_conat (n - S n0)) = false).
    { apply H. apply conat_lt_from_nat. omega. }
    rewrite H2.
    replace (cS (nat_to_conat (n - S n0))) with (nat_to_conat (n - n0)); swap 1 2.
    { unfold nat_to_conat. rewrite add_nat_to_conat_sub_1'; [|omega].
      f_equal. f_equal. omega. }
    rewrite <- H0; [|omega].
    rewrite <- add_nat_to_conat_sub_1 with (n := n - n0); [|omega].
    f_equal. omega.
Qed.

Lemma lt_inf_min :
  forall p : conat -> bool,
  (exists c, lt_inf c /\ p c = true) ->
  (exists c, (lt_inf c /\ p c = true /\ (forall d, conat_lt d c -> p d = false))).
Proof.
  (* TODO *)
  (* Should be provable... *)
Admitted.

Lemma root_lt_inf_correct :
  forall p : conat -> bool,
  (exists c, lt_inf c /\ p c = true) -> p (root p) = true.
Proof.
  intros. pose proof (lt_inf_min p H).
  destruct H0 as [c Hc].
  replace (root p) with c; [|symmetry; now apply root_lt_precise].
  apply Hc.
Qed.

Axiom lt_inf_or_not :
  forall p : conat -> bool,
  (exists c, is_true (p c)) ->
    ((exists c, lt_inf c /\ p c = true) \/ 
     ((forall c, lt_inf c -> p c = false) /\ p inf = true)).

Theorem root_correct :
  forall p : conat -> bool,
  (exists c, is_true (p c)) -> is_true (p (root p)).
Proof.
  intros. destruct (lt_inf_or_not p H).
  - now apply root_lt_inf_correct.
  - now rewrite conat_eq_fun with (c := root p) (d := inf); [|apply root_lt_inf_false].
Qed.