Require Export Setoid Morphisms.
Require Export equiv_on embed_nat Dec.
Notation "'if!' x 'is' p 'then' a 'else' b" := (match x with p => a | _ => b end) (at level 0, p pattern).
Notation "'fun!' '⟨' x ',' y '⟩' '=>' b" := (fun p => let (x,y) := unembed p in b) (at level 30, b at next level).
Notation "'∑' x .. y , p" := (sig (fun x => .. (sig (fun y => p)) ..))
(at level 200, x binder, right associativity,
format "'[' '∑' '/ ' x .. y , '/ ' p ']'")
: type_scope.
From Coq.Logic Require Import ConstructiveEpsilon.
Set Implicit Arguments.
Definition mu_nat_p := constructive_indefinite_ground_description_nat.
Lemma mu_nat_p_min P d H : forall m, m < proj1_sig (@mu_nat_p P d H) -> ~ P m.
Proof.
intros. unfold mu_nat_p, constructive_indefinite_ground_description_nat in *.
eapply linear_search_smallest. split. 2:eassumption. firstorder.
Qed.
Lemma mu_nat_p_least (P : nat -> Prop) d H : forall m, P m -> m >= proj1_sig (@mu_nat_p P d H).
Proof.
intros. unfold mu_nat_p, constructive_indefinite_ground_description_nat in *.
destruct (Compare_dec.le_lt_dec (proj1_sig (linear_search P d 0 (let (n, p) := H in O_witness P n (stop P n p)))) m).
eassumption. exfalso.
eapply linear_search_smallest. split. 2:eassumption. eapply le_0_n. eassumption.
Qed.
Lemma mu_nat_p_irrel (P : nat -> Prop) d H1 H2 : proj1_sig (@mu_nat_p P d H1) = proj1_sig (@mu_nat_p P d H2).
Proof.
eapply PeanoNat.Nat.le_antisymm; eapply mu_nat_p_least, proj2_sig.
Qed.
Definition mu_nat (f : nat -> bool) (H : exists n, f n = true) : nat.
Proof.
eapply mu_nat_p in H. eapply H. intros. decide equality.
Defined.
Definition mu_nat_spec (f : nat -> bool) (H : exists n, f n = true) : f (mu_nat f H) = true.
Proof.
unfold mu_nat. now destruct mu_nat_p.
Qed.
Opaque mu_nat.
Require Export equiv_on embed_nat Dec.
Notation "'if!' x 'is' p 'then' a 'else' b" := (match x with p => a | _ => b end) (at level 0, p pattern).
Notation "'fun!' '⟨' x ',' y '⟩' '=>' b" := (fun p => let (x,y) := unembed p in b) (at level 30, b at next level).
Notation "'∑' x .. y , p" := (sig (fun x => .. (sig (fun y => p)) ..))
(at level 200, x binder, right associativity,
format "'[' '∑' '/ ' x .. y , '/ ' p ']'")
: type_scope.
From Coq.Logic Require Import ConstructiveEpsilon.
Set Implicit Arguments.
Definition mu_nat_p := constructive_indefinite_ground_description_nat.
Lemma mu_nat_p_min P d H : forall m, m < proj1_sig (@mu_nat_p P d H) -> ~ P m.
Proof.
intros. unfold mu_nat_p, constructive_indefinite_ground_description_nat in *.
eapply linear_search_smallest. split. 2:eassumption. firstorder.
Qed.
Lemma mu_nat_p_least (P : nat -> Prop) d H : forall m, P m -> m >= proj1_sig (@mu_nat_p P d H).
Proof.
intros. unfold mu_nat_p, constructive_indefinite_ground_description_nat in *.
destruct (Compare_dec.le_lt_dec (proj1_sig (linear_search P d 0 (let (n, p) := H in O_witness P n (stop P n p)))) m).
eassumption. exfalso.
eapply linear_search_smallest. split. 2:eassumption. eapply le_0_n. eassumption.
Qed.
Lemma mu_nat_p_irrel (P : nat -> Prop) d H1 H2 : proj1_sig (@mu_nat_p P d H1) = proj1_sig (@mu_nat_p P d H2).
Proof.
eapply PeanoNat.Nat.le_antisymm; eapply mu_nat_p_least, proj2_sig.
Qed.
Definition mu_nat (f : nat -> bool) (H : exists n, f n = true) : nat.
Proof.
eapply mu_nat_p in H. eapply H. intros. decide equality.
Defined.
Definition mu_nat_spec (f : nat -> bool) (H : exists n, f n = true) : f (mu_nat f H) = true.
Proof.
unfold mu_nat. now destruct mu_nat_p.
Qed.
Opaque mu_nat.