Noetherian finite set

noeth.v

(* https://github.com/thery/grobner/blob/master/grobner.v#L1222 *)
(* http://firsov.ee/noeth/ Firsov, Uustalu, Veltri, [2016] "Variations on Noetherianness" *)

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

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive bar A (P : pred (seq A)) (l : seq A) : Prop :=
  | stop : P l -> bar P l
  | ask  : (forall a, bar P (a::l)) -> bar P l.

Definition noetherian (A : eqType) : Prop := @bar A (negb \o uniq) [::].

Lemma noetherian_bool : noetherian bool_eqType.
Proof.
apply: ask; case; apply: ask; case.
- by apply: stop.
- by apply: ask; case; apply: stop.
- by apply: ask; case; apply: stop.
by apply: stop.
Qed.

Inductive barS A (P : A -> pred (seq A)) (l : seq A) : Prop :=
  | askS : (forall a, P a l -> barS P (a :: l)) -> barS P l.

Definition noetherianS (A : eqType) : Prop := @barS A (fun h t => h \notin t) [::].

Lemma noetherianS_bool : noetherianS bool_eqType.
Proof.
apply: askS=>/=; case=>_; apply: askS=>/=; case=>/=.
- by [].
- by move=>_; apply: askS=>/=; case.
- by move=>_; apply: askS=>/=; case.
by [].
Qed.

Inductive barG A (P : A -> pred (seq A)) (l : seq A) : Prop :=
  | tellG : forall a, barG P (a::l) -> barG P l
  | askG  : (forall a, P a l -> barG P (a::l)) -> barG P l.

Definition noetherianG (A : eqType) : Prop := @barG A (fun h t => h \notin t) [::].

Lemma noetherianG_bool : noetherianG bool_eqType.
Proof.
apply: askG=>/=; case=>_.
- apply: (@tellG _ _ _ false).
  by apply: askG; case.
apply: (@tellG _ _ _ true).
by apply: askG; case.
Qed.

Inductive barE A (P : A -> pred (seq A)) (l : seq A) : Prop :=
  | stopE : (forall a, P a l) -> barE P l
  | tellE : forall a, barE P (a::l) -> barE P l
  | askE  : (forall a, barE P (a::l)) -> barE P l.

Definition noetherianE (A : eqType) : Prop := @barE A (fun h t => h \in t) [::].

Lemma noetherianE_bool : noetherianE bool_eqType.
Proof.
apply: askE=>/=; case.
- apply: (@tellE _ _ _ false).
  by apply: stopE; case.
apply: (@tellE _ _ _ true).
by apply: stopE; case.
Qed.