Karl Palmskog (Jul 15 2020 at 18:54): 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.
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?
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
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?
Paolo Giarrusso (Jul 15 2020 at 19:59):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). ;)
Li-yao (Jul 15 2020 at 20:09):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.
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...
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.
@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: Oct 13 2024 at 01:02 UTC