Stream: Coq users

Topic: Terminating functions on possibly-infinite data


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jul 15 2020 at 19:40):

wait, so depelim is part of Equations?

view this post on Zulip Kenji Maillard (Jul 15 2020 at 19:42):

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

view this post on Zulip Kenji Maillard (Jul 15 2020 at 19:43):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:54):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:55):

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

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:55):

maybe Equations overrides dependent induction to avoid K more often.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:57):

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

view this post on Zulip Karl Palmskog (Jul 15 2020 at 19:58):

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

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:59):

AFAIK yes

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:59):

the next thing is the manual encoding using remember or move

view this post on Zulip 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.

view this post on Zulip Li-yao (Jul 15 2020 at 20:04):

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

view this post on Zulip Karl Palmskog (Jul 15 2020 at 20:05):

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

view this post on Zulip Gaëtan Gilbert (Jul 15 2020 at 20:06):

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

view this post on Zulip Gaëtan Gilbert (Jul 15 2020 at 20:08):

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

view this post on Zulip Li-yao (Jul 15 2020 at 20:09):

hah nice

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jul 15 2020 at 23:45):

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

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 20:02 UTC