Skip to content

Instantly share code, notes, and snippets.

@kyoDralliam
Created March 18, 2022 12:44
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save kyoDralliam/73b270f18d6c2a0b5725fc73afc21d61 to your computer and use it in GitHub Desktop.
Accessibility and extraction of infinite decending chains
From Equations Require Import Equations.
From Coq Require Import ssreflect.
Section Defs.
Context {A : Type} (R : A -> A -> Prop).
Definition entire := forall x, exists y, R y x.
Definition idc_from a0 :=
exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).
Definition idc := exists f : nat -> A, forall n, R (f (S n)) (f n).
End Defs.
Definition dc_statement := forall A (R : A -> A -> Prop), entire R -> forall a0, idc_from R a0.
Lemma wf_not_idc {A : Type} (R : A -> A -> Prop) : well_founded R -> ~(idc R).
Proof.
move=> wfR [f hf].
apply (Fix (measure_wf wfR f)); last constructor.
move=> n h; apply: (h (S n)); apply: hf.
Qed.
Module not_wf_idc.
Context (em : forall (P : Prop), P \/ ~ P).
Context (dc : dc_statement).
Lemma dne : forall P, ~~P -> P.
Proof. move=> P; case: (em P)=> //. Qed.
Lemma neg_exists (A : Type) (P : A -> Prop) : ~ (exists a, P a) -> forall a, ~ P a.
Proof. move=> h a p; apply: h; exists a=> //. Qed.
Lemma em_forall (A : Type) (P : A -> Prop) : (forall a, P a) \/ exists a, ~ (P a).
Proof.
case: (em (forall a, P a)); [now left|right].
apply: dne=> /neg_exists h; apply: b=> x; exact (dne _ (h x)).
Qed.
Context (A : Type) R (h : ~(well_founded (A:=A) R)).
Lemma non_acc_pt : exists a, ~(Acc R a).
Proof. case: (em_forall A (Acc R))=> // /h []. Qed.
Definition Rstar := (Relation_Operators.clos_refl_trans A R).
Section LocalDef.
Context (a : A) (ha : ~(Acc R a)).
Definition B := { x : A | Rstar x a /\ ~(Acc R x) }.
Definition RB (x y : B) := R (proj1_sig x) (proj1_sig y).
Lemma entire_RB : entire RB.
Proof.
move=> [x [xa hx]].
case: (em_forall A (fun y => ~ (R y x) \/ Acc R y)).
- move=> h0; exfalso; apply hx; constructor=> z accz.
case: (h0 z)=> // /(_ accz) [].
- move=> [y0] /Decidable.not_or [/dne desc hy0].
unshelve eexists (exist _ y0 _).
1: split=> //; eapply Relation_Operators.rt_trans; last eassumption;
by constructor.
assumption.
Qed.
End LocalDef.
Lemma inf_desc_chain : idc R.
Proof.
case: non_acc_pt=> [a ha].
have a' : B a by exists a; split=> //; constructor.
move: (dc (B a) (RB a) (entire_RB a) a') => [f [_ hf]].
exists (fun n => proj1_sig (f n)) => //.
Qed.
End not_wf_idc.
Module not_wf_idc_dc.
Context (not_wf_idc : forall A (R : A -> A -> Prop), ~(well_founded R) -> idc R).
Context A (R : A -> A -> Prop) (eR : entire R).
Section Local.
Context (a0 : A).
Definition Rstar := (Relation_Operators.clos_refl_trans A R).
Definition B := { x : A | Rstar x a0 }.
Definition RB (x y : B) := R (proj1_sig x) (proj1_sig y).
Lemma not_acc (b : B) : ~(Acc RB b).
Proof.
elim=> -[x hx] h ih; move: (eR x)=> [y hy].
refine (ih (exist _ y _) hy).
eapply Relation_Operators.rt_trans; last eassumption; by constructor.
Qed.
Lemma not_wf : ~(well_founded RB).
Proof.
have a1 : B by exists a0; by constructor.
move=> /(_ a1); apply: not_acc.
Qed.
End Local.
Lemma reduce_idc_from a0 (b : B a0) : (idc_from (RB a0) b) -> (idc_from R a0).
Proof.
move: b=> [? h].
move=> [g [geq0 hg]].
have h' := (Operators_Properties.clos_rt_rt1n _ _ _ _ h).
move: {geq0}g (f_equal (@proj1_sig _ _) geq0) hg => /= {h}.
induction h'.
+ move=> g geq0 hg; exists (fun n => proj1_sig (g n))=> //.
+ move=> gx geqx hgx.
unshelve apply: IHh'.
* case=>[|n]; [| exact (gx n)].
exists y; by apply: Operators_Properties.clos_rt1n_rt.
* reflexivity.
* case=>[|n] /=; last apply: hgx.
rewrite /RB geqx //=.
Qed.
Lemma dc : forall a0, exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).
Proof.
move=> a0.
move: (not_wf_idc (B a0) (RB a0) (not_wf a0))=> [g hg].
apply: (reduce_idc_from a0 (g 0)); exists g; split=> //.
Qed.
End not_wf_idc_dc.
Module not_wf_idc_dne.
Context (not_wf_idc : forall A (R : A -> A -> Prop), ~(well_founded R) -> idc R).
Context (P : Prop).
Definition RP (x y : unit) := P.
Lemma not_wf_RP : ~~P -> ~(well_founded RP).
Proof.
move=> nnp wfRP; apply: nnp=> p.
induction (wfRP tt). exact (H0 tt p).
Qed.
Lemma dne : ~~P -> P.
Proof.
move=> /not_wf_RP /not_wf_idc [? hf].
exact (hf 0).
Qed.
End not_wf_idc_dne.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment