## Stream: Coq users

### Topic: Terminating functions on possibly-infinite data

#### Karl Palmskog (Jul 15 2020 at 18:54):

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.
``````

#### Kenji Maillard (Jul 15 2020 at 19:38):

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.
``````

#### Karl Palmskog (Jul 15 2020 at 19:40):

wait, so depelim is part of Equations?

#### Kenji Maillard (Jul 15 2020 at 19:43):

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

#### Karl Palmskog (Jul 15 2020 at 19:48):

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.

#### Kenji Maillard (Jul 15 2020 at 19:49):

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)

#### Paolo Giarrusso (Jul 15 2020 at 19:54):

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

#### Karl Palmskog (Jul 15 2020 at 19:55):

`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.

#### Paolo Giarrusso (Jul 15 2020 at 19:55):

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

#### Paolo Giarrusso (Jul 15 2020 at 19:55):

maybe Equations overrides `dependent induction` to avoid K more often.

#### Paolo Giarrusso (Jul 15 2020 at 19:57):

and FWIW, `Require Import Program.` loads even funext and proof irrelevance

#### Karl Palmskog (Jul 15 2020 at 19:58):

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

AFAIK yes

#### Paolo Giarrusso (Jul 15 2020 at 19:59):

the next thing is the manual encoding using `remember` or `move`

#### Paolo Giarrusso (Jul 15 2020 at 20:00):

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.`

#### Li-yao (Jul 15 2020 at 20:04):

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

#### Karl Palmskog (Jul 15 2020 at 20:05):

yes, one can't even interactively define a `Fixpoint` on coinductives like that, Coq refuses

#### Gaëtan Gilbert (Jul 15 2020 at 20:06):

basically `match x with C y => y end` is smaller than `x`

#### Gaëtan Gilbert (Jul 15 2020 at 20:08):

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

hah nice

#### Karl Palmskog (Jul 15 2020 at 20:21):

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.
``````

#### Karl Palmskog (Jul 15 2020 at 22:36):

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.
``````

#### Paolo Giarrusso (Jul 15 2020 at 23:37):

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

#### Karl Palmskog (Jul 15 2020 at 23:45):

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

#### Kenji Maillard (Jul 16 2020 at 06:20):

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.
``````

#### Karl Palmskog (Jul 16 2020 at 08:14):

@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: May 18 2024 at 08:40 UTC