The Coq mailing list

[Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>]

    Dear Burak,
    
    You do not give the definition of coseq,
    but I expect you axiom is incosistent: it
    implies the cosequence is finite, while ct
    can hold for infinite sequences. Given the name you give to the
    axiom you seem to expect this is a form of extensionality. Where
    does this idea come from? I never saw extensionality expressed in
    this way.
    
    Here is the Coq proof:
    
    Require Import List.
    
    Import ListNotations.
    
    CoInductive coseq {A : Type} : Type :=
      | conil : coseq
      | cocons : A -> coseq -> coseq.
    
    Arguments coseq : clear implicits.
    
    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.
    
    Fixpoint drop (n : nat) {A : Type} (c : coseq A) {struct n} : option
    (coseq A) :=
      match n, c with
      | 0, c => Some c
      | S _, conil => None
      | S n', cocons _ c' => drop n' c'
      end.
    
    Definition finite {A : Type} (c : coseq A) := exists n, drop n c =
    None.
    
    Lemma it_finite {A : Type} (c : coseq A) (l : list A) : it c l ->
    finite c.
    Proof.
      induction 1.
      - exists 1 ; reflexivity.
      - destruct IHit as [n ?].
        exists (S n).
        cbn.
        assumption.
    Qed.
    
    CoFixpoint ones : coseq nat := cocons 1 ones.
    
    Definition hd {A} (s : coseq A) : option A :=
      match s with
      | conil => None
      | cocons x _ => Some x
      end.
    
    Definition tl {A} (s : coseq A) : option (coseq A) :=
      match s with
      | conil => None
      | cocons _ s' => Some s'
      end.
    
    Lemma eta_coseq {A} (s : coseq A) :
      match (hd s), (tl s) with
      | None, None => s = conil
      | Some h, Some t => s = cocons h t
      | _, _ => False
      end.
    Proof.
      case s; simpl; reflexivity.
    Qed.
    
    Lemma ones_unfold : _ones_ = cocons 1 ones.
    Proof.
      exact (eta_coseq ones).
    Qed.
    
    Lemma ct_ones : ct ones [1].
    Proof.
      cofix CH.
      rewrite ones_unfold.
      constructor ; [..| assumption].
      now constructor.
    Qed.
    
    Lemma ones_infinite : finite ones -> False.
    Proof.
      intros [n Hn].
      induction n.
      - cbn in * ; congruence.
      - now cbn in *.
    Qed.
    
    Axiom ext: forall {A: Type} xs ys, ct xs ys -> @it A xs ys.
    
    Theorem boom : False.
    Proof.
      eapply ones_infinite, it_finite, ext, ct_ones.
    Qed.
    
    Best,
Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 13/03/2024 12:15, Burak Ekici wrote:

DB4PR10MB60466E5063C236BBA9696A8ACD2A2 AT DB4PR10MB6046.EURPRD10.PROD.OUTLOOK.COM">

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