Existential Witness Operators aka nat choice

ewo.v

Require Extraction.
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype seq.

(* https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf#chapter.25 *)

Inductive A : Prop := AA of (True -> A).

Definition exf : A -> False.
Proof. by elim. Qed.

Section EWO.

Variable p : pred nat.

(* linear search type *)
Inductive T n : Prop := C of (~~ p n -> T n.+1).

Definition W' : forall n, T n -> {m | p m} :=
  fix F n (a : T n) :=
  let: C phi := a in
  match (boolP (p n)) with
  | AltTrue H => exist p n H
  | AltFalse H => F n.+1 (phi H)
  end.

Lemma Tbase n : p n -> T n.
Proof. by move=>H; constructor; rewrite H. Qed.

Lemma Tstep n : T n.+1 -> T n.
Proof. by move=>H; constructor. Qed.

Lemma Tzero n : T n -> T 0.
Proof.
elim: n; first by [].
by move=>n IH H1; apply: IH; apply: Tstep.
Qed.

Fact Tstep_add k n : T (k + n) -> T n.
Proof.
elim: k=>[|k IH]; first by [].
by rewrite addSn =>/Tstep.
Qed.

Lemma V : forall n, p n -> T 0.
Proof.
by move=>n Hn; apply: (Tzero n); apply: Tbase.
Qed.

Lemma W : (exists n, p n) -> {m | p m}.
Proof.
move=>H; apply: (W' 0).
by case: H=>x /V.
Qed.

End EWO.

Section Least.

Definition safe (p : pred nat) n := forall k, p k -> k >= n.
Definition least (p : pred nat) n := p n /\ safe p n.

Lemma least_unique p n m : least p n -> least p m -> n = m.
Proof.
case=>Hn1 Hn2; case=>Hm1 Hm2.
move: (Hn2 m Hm1)=>Hnm; move: (Hm2 n Hn1)=>Hmn.
by apply/eqP; rewrite eqn_leq Hnm Hmn.
Qed.

Lemma safe_S p n : safe p n -> ~~ p n -> safe p n.+1.
Proof.
move=>H Hp k Hk.
move: (H k Hk); rewrite leq_eqVlt; case/orP=>//.
by move/eqP=>E; rewrite E Hk in Hp.
Qed.

Lemma least_direct_sigma' p n : safe p n + {m | least p m}.
Proof.
elim: n; first by left.
move=>n; case.
- move=>H; case/boolP: (p n)=>Hp.
  - by right; exists n.
  by left; apply: safe_S.
by move=>Hm; right.
Qed.

Lemma least_direct_sigma (p : pred nat) : {x : nat | p x} -> {x : nat | least p x}.
Proof.
case=>n Hn; case: (least_direct_sigma' p n)=>//.
by move=>H; exists n.
Qed.

Corollary least_direct_ex (p : pred nat) : (exists x : nat, p x) -> (exists x : nat, least p x).
Proof.
case=>x Hx.
case: (least_direct_sigma _ (exist _ x Hx))=>y Hy.
by exists y.
Qed.

Lemma least_dec p n : decidable (least p n).
Proof.
case/boolP: (p n)=>Hp.
- case: (least_direct_sigma _ (exist _ n Hp))=>x Hx.
  case/boolP: (x==n).
  - by move/eqP=><-; left.
  move=>Hxn; right=>Hn.
  by move: (least_unique _ _ _ Hn Hx)=>E; rewrite E eq_refl in Hxn.
by right; case=>Hp'; rewrite Hp' in Hp.
Qed.

Lemma W_least_1 (p : pred nat) : (exists n, p n) -> {m | least p m}.
Proof. by move/W/least_direct_sigma. Qed.

Lemma W_least_2 (p : pred nat) : (exists n, p n) -> {m | least p m}.
Proof.
case/W=>m Hm.
move: (least_direct_ex _ (ex_intro _ m Hm))=>Hl.
have Hl': exists x : nat, least_dec p x.
- by case: Hl=>x Hx; exists x; apply/sumboolP.
by case: (W _ Hl')=>x /sumboolP Hx; exists x.
Qed.

End Least.

Section Binary.

Definition next '(x, y) : nat * nat :=
  if x is k.+1 then (k, y.+1) else (y.+1, 0).

Fixpoint decode n : nat * nat :=
  if n is k.+1
    then next (decode k)
    else (0,0).

Definition sum n : nat :=
  sumn (rev (iota 0 n.+1)).

Lemma sumS n : sum n.+1 = sum n + n.+1.
Proof.
rewrite {2}(_ : n.+1 = sumn (rev (iota n.+1 1))); last by rewrite /= addn0.
by rewrite /sum addnC -sumn_cat -rev_cat -{3}(add0n n.+1) -iotaD addn1.
Qed.

Definition encode '(x, y) : nat :=
  sum (x + y) + y.

Fact encode_next a :
  encode (next a) = (encode a).+1.
Proof.
case: a; case=>[|x] y /=.
- rewrite !addn0 add0n -[RHS]addn1 -addnA addn1.
  by exact: sumS.
by rewrite !addnS addSn.
Qed.

Lemma encode0 a : encode a = 0 -> a = (0, 0).
Proof.
case: a; case=>[|a]; case=>[|b] //=.
- by rewrite addnS.
- by rewrite !addn0 sumS addnS.
by rewrite addnS.
Qed.

(* Disable simplification of encode *)
Opaque encode.

Fact encode_decode n :
  encode (decode n) = n.
Proof.
elim: n=>//= n IH.
by rewrite encode_next IH.
Qed.

Lemma decode_encode' n a : encode a = n -> decode n = a.
Proof.
elim: n a=>/=.
- by move=>a; move/encode0.
move=>n IH; case=>x; case=>[|y].
- case: x=>// x.
  rewrite (_ : (x.+1,0) = next (0, x)) // encode_next.
  by case=>/IH ->.
rewrite (_ : (x, y.+1) = next (x.+1, y)) // encode_next.
by case=>/IH->.
Qed.

Fact decode_encode a :
  decode (encode a) = a.
Proof. by apply: (decode_encode' (encode a) a). Qed.

Lemma W_bin (p : rel nat) : (exists n m, p n m) -> {n & { m | p n m}}.
Proof.
move=>H; pose q n := p (decode n).1 (decode n).2.
have/W : exists n : nat, q n.
- case: H=>n[m Hnm]; exists (encode (n,m)).
  by rewrite /q decode_encode.
case=>x; rewrite /q=>Hp.
by exists (decode x).1, (decode x).2.
Qed.

End Binary.

Section Disjunctive.

Lemma W_disj (p q : pred nat) :
  (exists n, p n) \/ (exists m, q m) -> {n | p n} + {m | q m}.
Proof.
move=>H.
have/W : (exists n, p n || q n).
- by case: H; case=>x H; exists x; rewrite H // orbT.
case=>x; case/boolP: (p x)=>/=.
- by move=>Hp _; left; exists x.
by move=>_ Hq; right; exists x.
Qed.

End Disjunctive.

Section StepIndexed.

Variable X: Type.
Variable f: X -> X -> pred nat.
Variable f_prop: forall x y, x = y <-> exists n, f x y n.

Lemma decX (x y : X) : decidable (x = y).
Proof.
suff: { n | f x x n }; last by apply/W/f_prop.
case=>n H; case/boolP: (f x y n)=>Hxy.
- by left; apply/f_prop; exists n.
by right=>E; rewrite -E H in Hxy.
Qed.

End StepIndexed.


Section InfinitePath.

Variable p : rel nat.
Variable p_total : forall x, exists y, p x y.

Definition f (x : nat) : nat := sval (W (p x) (p_total x)).

Lemma p_f x : p x (f x).
Proof.
by rewrite /f; case: (W (p x) (p_total x))=>y H.
Qed.

Variable x : nat.

Fixpoint fp (n : nat) : nat :=
  if n is k.+1 then
    let y := fp k in
    f y
  else x.

Lemma fp0 : fp 0 = x.
Proof. by []. Qed.

Lemma f_path n : p (fp n) (fp n.+1).
Proof. by apply: p_f. Qed.

End InfinitePath.

Section Ge.

Variable p : pred nat.

Lemma W_gt : forall n, T p n -> {k | (n <= k) && p k}.
Proof.
refine (
  fix FF n (a : T p n) {struct a} :=
  let: C phi := a in
  match (boolP (p n)) with
  | AltTrue H => _
  | AltFalse H => _
  end).
- by exists n; rewrite leqnn.
case: (FF n.+1 (phi H))=>x; case/andP=>Hx Hpx.
by exists x; rewrite Hpx andbT; apply/ltnW.
Qed.

End Ge.

Section Bool.

Variable p : pred bool.

Lemma W_bool : (exists b, p b) -> {c | p c}.
Proof.
move=>H.
case Et: (p true); first by exists true.
case Ef: (p false); first by exists false.
by exfalso; case: H; case; [rewrite Et | rewrite Ef].
Qed.

End Bool.

Section Eliminator.

Variable p : pred nat.

Print T_rect.

Definition T_elim (q : nat -> Type) :
  (forall n, (~~ p n -> q n.+1) -> q n) ->
  forall n, T p n -> q n :=
  fun f => fix F (n : nat) (t : T p n) {struct t}  :=
  let: (C phi) := t in
  f n (fun h => F n.+1 (phi h)).

Definition W'' : forall n, T p n -> {m | p m} :=
  T_elim
   (fun=> {m : nat | p m})
   (fun (n : nat) (f : ~~ p n -> {m : nat | p m}) =>
    match boolP (p n) with
    | AltTrue H => exist p n H
    | AltFalse H => f H
    end).

Fact T_ex_ge n : T p n <-> exists k, k >= n /\ p k.
Proof.
split.
- elim/T_elim=>{}n.
  case/boolP: (p n)=>Hp /=.
  - by move=>_; exists n.
  by move=>/(_ erefl); case=>k [H H2]; exists k; split=>//; apply: ltnW.
case=>k [H H2]; apply: (Tstep_add _ (k-n)).
rewrite -(addnABC H); last by [].
by rewrite subnn addn0; apply: Tbase.
Qed.

End Eliminator.

Section AccFrom.

Variable p : pred nat.

(* https://github.com/anton-trunov/csclub-coq-course-spring-2021/blob/master/lectures/count_up.v *)

Inductive acc_from i : Prop :=
| AccNow of p i
| AccLater of acc_from i.+1.

Lemma accT i : acc_from i <-> T p i.
Proof.
split.
- elim=>{}i.
  - by apply: Tbase.
  by move=>_; apply: Tstep.
elim/T_elim=>{}i IH.
case/boolP: (p i)=>Hp.
- by apply: AccNow.
by apply/AccLater/IH.
Qed.

End AccFrom.