So I want to define a bunch of terminating (`Fixpoint`

) functions on possibly-infinite, i.e., coinductive, data. However, the proof effort diverges to some seriously annoying dependent elimination problems, and a naive application of Equations seems unhelpful, since I can only show "conditional" well-foundedness. There is probably some much better way I'm missing.

I wrote up a minimized example below. Any help appreciated, and I will probably do some short writeup on the Discourse if I figure this out properly.

```
From Coq Require Import ssreflect.
From Coq Require Import Lia.
Require Coq.Program.Wf.
CoInductive trace : Set :=
| Tnil : trace
| Tcons : trace -> trace.
Inductive finite_Set : trace -> Set :=
| finite_Set_nil: finite_Set Tnil
| finite_Set_delay: forall tr,
finite_Set tr -> finite_Set (Tcons tr).
(* easy! *)
Fixpoint id_finite_Set (tr : trace) (h : finite_Set tr) :=
match h with
| finite_Set_nil => tr
| finite_Set_delay tr' Hfin =>
id_finite_Set tr' Hfin
end.
(* we need impredicativity! *)
Inductive finite : trace -> Prop :=
| finite_nil: finite Tnil
| finite_delay: forall tr,
finite tr -> finite (Tcons tr).
Fail Fixpoint id_finite (tr : trace) (h : finite tr) :=
match h with
| finite_nil => tr
| finite_delay tr' Hfin =>
id_finite tr' Hfin
end.
(*
Incorrect elimination of "h" in the inductive type "finite":
the return type has sort "Set" while it should be "SProp" or "Prop".
*)
Definition finite_dec (tr : trace) (h: finite tr) :
{ tr' : trace | tr = Tcons tr' /\ finite tr' }+{ tr = Tnil }.
destruct tr.
- by right.
- left; exists tr.
by inversion h; subst.
Defined.
Fail Fixpoint id_finite (tr : trace) (h : finite tr) { struct h } :=
match finite_dec tr h with
| inleft (exist tr' (conj Heq Hfin)) =>
id_finite tr' Hfin
| inright _ => Tnil
end.
(*
Recursive call to id_finite has principal argument equal to "Hfin" instead of
a subterm of "h".
*)
(* OK, so let's define an "easy" measure *)
Inductive len_trace : trace -> nat -> Prop :=
| len_trace_nil : len_trace Tnil 0
| len_trace_delay : forall tr n,
len_trace tr n -> len_trace (Tcons tr) (S n).
Lemma finite_len_trace : forall tr, finite tr -> exists n, len_trace tr n.
Proof.
move => tr; elim; first by exists 0; exact: len_trace_nil.
move => tr' Hfin [n Hn].
by exists (S n); exact: len_trace_delay.
Qed.
Lemma len_trace_unique : forall tr n0,
len_trace tr n0 ->
forall n, len_trace tr n ->
n = n0.
Proof.
move => tr n0.
elim; first by move => n Hlt; inversion Hlt.
move => tr' n1 Hl IH n Hlen.
inversion Hlen; subst.
apply IH in H0.
by apply eq_S.
Qed.
Definition finite_lt (tr tr' : trace) :=
exists n n', len_trace tr n /\ len_trace tr' n' /\ n < n'.
Lemma same_len_trace_Acc : forall n0 tr tr',
Acc finite_lt tr ->
len_trace tr' n0 ->
len_trace tr n0 ->
Acc finite_lt tr'.
Proof.
elim.
- move => tr tr' Hacc Hl Hl'.
inversion Hl; subst.
apply: Acc_intro.
move => tr0. case => n; case => n'; case => [Hn [Hn' Hlt]].
inversion Hn'; subst.
by inversion Hlt.
- move => n IH tr tr' Hacc Hl Hl'.
inversion Hl; subst.
inversion Hl'; subst.
apply Acc_intro.
move => t Hlt.
inversion Hlt.
case: H => [n' [Hn [Hn' Hlt']]].
inversion Hn'; subst.
inversion Hacc.
apply H.
exists x; exists (S n).
split => //; split => //.
inversion Hn'; subst.
by have ->: n = n0 by apply (len_trace_unique _ _ H0).
Qed.
Lemma finite_lt_Acc : forall tr : trace, finite tr -> Acc finite_lt tr.
Proof.
move => tr.
elim.
- apply Acc_intro.
move => tr'; case => n; case => n'; case => [Hn [Hn' Hlt]].
inversion Hn'; subst.
by inversion Hlt.
- move => tr0 Hf Ha.
inversion Ha.
apply Acc_intro => tr' Hf'.
inversion Hf'.
case: H0 => [n [Htr [Htr' Hlt]]].
inversion Htr'; subst.
have Heq: x = n0 \/ x < n0 by lia.
case: Heq; last by move => Hlt'; apply H; exists x; exists n0.
move => Heq.
subst.
apply: same_len_trace_Acc.
* by apply Ha.
* by apply Htr.
* by apply H1.
Qed.
(* OK, let's prove this with Program Fixpoint *)
Program Fixpoint id_finite (tr : trace) (h : finite tr) { wf finite_lt tr } :=
match finite_dec tr h with
| inleft (exist _ tr' (conj Heq Hfin)) =>
id_finite tr' Hfin
| inright _ => Tnil
end.
Next Obligation.
case (finite_len_trace _ Hfin) => n Hl.
exists n; exists (S n).
split => //; split.
- by apply len_trace_delay.
- by constructor.
Defined.
Next Obligation.
case => tr.
Fail elim.
(* crazy dependent elimination seemingly required *)
Abort.
```

Wouldn't that solution using Equations fit the bill ?

```
From Equations Require Import Equations.
Derive Signature for finite.
Definition invert_finite_delay (tr : trace) (h : finite (Tcons tr)) : finite tr.
Proof.
depelim h; [discriminate| injection H; move=> -> //].
Defined.
Fixpoint id_finite (tr : trace) (h : finite tr) {struct h} : trace :=
match tr with
| Tnil => fun _ => Tnil
| Tcons tr => fun h => id_finite tr (invert_finite_delay tr h)
end h.
```

wait, so depelim is part of Equations?

It seems it is redefined when loading Equations: https://github.com/mattam82/Coq-Equations/blob/master/theories/Prop/Tactics.v

but yes the depelim in my code above is coming from Equations

ah, it seems it could be done without Equations anyway:

```
Require Import Coq.Program.Equality.
Definition invert_finite_delay (tr : trace) (h : finite (Tcons tr)) : finite tr.
Proof.
by dependent destruction h.
Defined.
Fixpoint id_finite (tr : trace) (h : finite tr) {struct h} : trace :=
match tr with
| Tnil => fun _ => Tnil
| Tcons tr => fun h => id_finite tr (invert_finite_delay tr h)
end h.
```

But thanks a lot @Kenji Maillard, the `Defined`

stuff is pure magic to me.

Without `Defined`

there is no way `id_finite`

could pass the guard condition (not that I understand how this program manages to pass the guard condition though)

@Karl Palmskog without Equations you might end up using axiom K needlessly

`Print Assumptions id_finite.`

says: `Closed under the global context`

with the `dependent induction`

solution.

But thanks for the heads up, didn't know it had this problem.

ah cool — but it's not guaranteed, it depends on the use.

maybe Equations overrides `dependent induction`

to avoid K more often.

and FWIW, `Require Import Program.`

loads even funext and proof irrelevance

but basically this is the only way to do dependent induction easily without Equations, right?

AFAIK yes

the next thing is the manual encoding using `remember`

or `move`

I'm fine with dependent induction and K, but if you really care, either add an output test, or use `move E: (Tcons tr) => foo. induction h; subst.`

That looks like some really magical behavior of the guard condition!

yes, one can't even interactively define a `Fixpoint`

on coinductives like that, Coq refuses

basically `match x with C y => y end`

is smaller than `x`

here is another fun fixpoint `Fixpoint foo (x:False) : nat := foo (match x with end).`

;)

hah nice

This is how it turned out in the real-world setting:

```
Definition invert_fin_delay
(tr : trace) (st st0 : state) (h : fin (Tcons st tr) st0) : fin tr st0.
Proof.
by dependent destruction h.
Defined.
Fixpoint cut (tr0: trace) (st0: state) (h: fin tr0 st0) (tr1: trace) { struct h }: trace :=
match tr0 as tr0' return (fin tr0' st0 -> trace) with
| Tnil _ => fun _ => tr1
| Tcons st tr => fun h' =>
match tr1 with
| Tnil _ => tr1
| Tcons st1 tr1' => cut (invert_fin_delay h') tr1'
end
end h.
```

it seems I can never be on friendly terms with dependent elimination. Shouldn't this be provable using dependent induction?

```
Lemma finite_depind : forall tr (h h':finite tr), id_finite tr h = id_finite tr h'.
Proof.
dependent induction h using finite_ind.
(* Error: Abstracting over the term "tr" leads to a term ... which is ill-typed *)
Abort.
CoInductive bisim: trace -> trace -> Prop :=
| bisim_nil: bisim Tnil Tnil
| bisim_cons: forall tr tr',
bisim tr tr' ->
bisim (Tcons tr) (Tcons tr').
Lemma finite_bisim_depind : forall tr (h h':finite tr), bisim (id_finite tr h) (id_finite tr h').
Proof.
dependent induction h using finite_ind.
(* Error: Abstracting over the term "tr" leads to a term ... which is ill-typed *)
Abort.
```

Program’s dependent induction also has some extra bugs compared to Equations... OTOH I thought it didn’t handle either using or automatic introduction...

same results with a slightly different error message when using Equations and `depind`

, unfortunately

Using Equations another time:

```
Derive NoConfusion for trace.
Lemma finite_depind : forall tr (h h':finite tr), id_finite tr h = id_finite tr h'.
Proof.
refine (fix IH tr h {struct h} := _).
case: tr h => [|tr] h; depelim h; try discriminate; move=> h' ; depelim h'=> //=.
Qed.
```

@Kenji Maillard thanks again for showing the idiom, here's the non-Equations version:

```
Lemma id_finite_eq : forall tr (h h':finite tr), id_finite tr h = id_finite tr h'.
Proof.
refine (fix IH tr h {struct h} := _).
case: tr h => [|tr] h.
- by depelim h; move => h'; depelim h'; simpl; reflexivity.
- by depelim h; move => h'; depelim h'; simpl; apply IH.
Qed.
```

Last updated: Feb 04 2023 at 20:02 UTC