The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hi Burak,

The property you stated is contradictory. The issue is that the it
predicate forces the first argument to be finite, whereas ct can hold
for some infinite coseqs. See the following attached file for a proof.

Best wishes,

On Wed, Mar 13, 2024 at 8:15 AM Burak Ekici <ekcburak AT hotmail.com> wrote:
>
> Dear all,
>
> I have a pair of predicates — one inductively and the other coinductively 
> defined as follows:
>
> CoInductive ct {A: Type}: coseq A -> list A -> Prop :=
>   | co_nil : forall ys, ct conil ys
>   | co_incl: forall x xs ys, List.In x ys -> ct xs ys -> ct (cocons x xs) 
> ys.
>
> Inductive it {A: Type}: coseq A -> list A -> Prop :=
>   | ci_nil : forall ys, it conil ys
>   | ci_incl: forall x xs ys, List.In x ys -> it xs ys -> it (cocons x xs) 
> ys.
>
> Would assuming an axiom like
>
> Axiom ext: forall {A: Type} xs ys, ct xs ys -> @it A xs ys.
>
> introduce any unsoundness?
>
> Thank you so much.
>
> Best,
>
> ―
>
> Burak



-- 
Arthur Azevedo de Amorim
Require Import Coq.Lists.List.
Import ListNotations.

Set Implicit Arguments.

CoInductive coseq (A : Type) : Type :=
| conil : coseq A
| cocons : A -> coseq A -> coseq A.

Arguments conil {A}.

CoInductive ct {A: Type}: coseq A -> list A -> Prop :=
  | co_nil : forall ys, ct conil ys
  | co_incl: forall x xs ys, List.In x ys -> ct xs ys -> ct (cocons x xs) ys.

Inductive it {A: Type}: coseq A -> list A -> Prop :=
  | ci_nil : forall ys, it conil ys
  | ci_incl: forall x xs ys, List.In x ys -> it xs ys -> it (cocons x xs) ys.

Axiom ext: forall {A: Type} xs ys, ct xs ys -> @it A xs ys.

Lemma coseq_eq {A : Type} (xs : coseq A) :
  xs = match xs with conil => conil | cocons x xs => cocons x xs end.
Proof. now destruct xs. Qed.

CoFixpoint const {A : Type} (x : A) : coseq A :=
  cocons x (const x).

Lemma const_eq {A : Type} (x : A) : const x = cocons x (const x).
Proof.
now rewrite (coseq_eq (const x)) at 1.
Qed.

Lemma in_singleton {A : Type} (x : A) : List.In x [x].
Proof. simpl. eauto. Qed.

Lemma ct_singleton {A : Type} (x : A) : ct (const x) [x].
Proof.
cofix H.
rewrite const_eq.
apply co_incl; trivial.
apply in_singleton.
Qed.

Fixpoint coseq_of_list {A : Type} (xs : list A) : coseq A :=
  match xs with
  | [] => conil
  | x :: xs => cocons x (coseq_of_list xs)
  end.

Lemma it_finite {A : Type} (xs : coseq A) ys :
  it xs ys -> exists xs', xs = coseq_of_list xs'.
Proof.
intros H.
induction H as [|x xs ys Hx _ [xs' IH]].
- now exists nil.
- exists (x :: xs'). simpl. now rewrite <- IH.
Qed.

Lemma contra : False.
Proof.
assert (exists xs, const tt = coseq_of_list xs) as [xs H].
{ eapply it_finite. apply ext. apply ct_singleton. }
induction xs as [|[] xs IH].
- rewrite const_eq in H. now simpl in H.
- rewrite const_eq in H. simpl in H.
  apply IH.
  congruence.
Qed.