funelim badly generalising, yields ill-typed goals

[TheoWinterhalter]

Hard to minimise so the error can be checked out at this commit.

After the use of funelim, I have an ill-typed induction hypothesis in one of my goals.

H: ∀ (x : context) (x0 : term),
      size x0 < size t
      → ∀ r : nat → nat,
          renaming x x0 r → rename r (rho x x0) = rho x0 (rename r x0)

The problem disappears if I use apply_funelim or revert the argument that is wrongly generalised before using funelim.

[eponier]

I think I encountered a similar problem. Here is the code:

Require Import Arith List Lia.
From Equations Require Import Equations.
Import ListNotations.

Inductive Subseq {A : Type} : list A -> list A -> Prop :=
| Subseq_nil : Subseq [] []
| Subseq_take : forall a xs ys, Subseq xs ys -> Subseq (a :: xs) (a :: ys)
| Subseq_drop : forall a xs ys, Subseq xs ys -> Subseq xs (a :: ys).

Definition IsLCS {A : Type} (zs xs ys : list A) : Prop :=
  Subseq zs xs /\ Subseq zs ys /\
  forall zs', Subseq zs' xs -> Subseq zs' ys -> length zs' <= length zs.

Equations lcs {A : Type} (eq_dec : forall x y : A, {x = y} + {x <> y})
          (l1 l2 : list A) : list A by wf (length l1 + length l2) lt :=
  lcs _ [] _ := [];
  lcs _ _ [] := [];
  lcs _ (x :: l1) (y :: l2) := 
    if eq_dec x y then x :: lcs eq_dec l1 l2 else
      let s1 := lcs eq_dec (x :: l1) l2 in
      let s2 := lcs eq_dec l1 (y :: l2) in
      if length s1 <? length s2 then s2 else s1.
Next Obligation. simpl; lia. Qed.
Next Obligation. simpl; lia. Qed.

Lemma Subseq_nil_l : forall {A} (l : list A), Subseq [] l.
Proof.
  induction l.
  - constructor.
  - constructor. assumption.
Qed.

Lemma Subseq_elim_cons_l : forall {A} a (l1 l2 : list A),
  Subseq (a :: l1) l2 -> Subseq l1 l2.
Proof.
  intros. revert dependent a. induction l2; intros.
  - inversion H.
  - inversion H; subst.
    + constructor. assumption.
    + constructor. eapply IHl2. eassumption.
Qed.

Lemma Subseq_elim_cons : forall {A} a1 a2 (l1 l2 : list A),
  Subseq (a1 :: l1) (a2 :: l2) -> Subseq l1 l2.
Proof.
  intros. inversion H; subst.
  - assumption.
  - apply Subseq_elim_cons_l in H2. assumption.
Qed.

Lemma Subseq_elim_cons_neq : forall {A} a1 a2 (l1 l2 : list A),
  a1 <> a2 ->
  Subseq (a1 :: l1) (a2 :: l2) -> Subseq (a1 :: l1) l2.
Proof.
  intros. inversion H0; subst.
  - contradiction.
  - assumption.
Qed.

Theorem lcs_correct : forall {A : Type} (eq_dec : forall x y : A, {x = y} + {x <> y}) xs ys,
  IsLCS (lcs eq_dec xs ys) xs ys.
Proof.
  (* Strangely, [funelim (lcs eq_dec xs ys)] does not go through [Qed]. *)
  apply lcs_elim with (P := fun _ _ xs ys l => IsLCS l xs ys); intros.
  - split; [|split].
    + constructor.
    + apply Subseq_nil_l.
    + intros. inversion H; subst. apply le_0_n.
  - split; [|split].
    + apply Subseq_nil_l.
    + constructor.
    + intros. inversion H0; subst. apply le_n.
  - destruct (eq_dec a a0).
    + specialize (H e). destruct H as (HH1 & HH2 & HH3).
      subst.
      split; [|split].
      * constructor. assumption.
      * constructor. assumption.
      * intros. destruct zs'.
        -- apply le_0_n.
        -- apply Subseq_elim_cons in H.
           apply Subseq_elim_cons in H2.
           cbn. apply le_n_S. eauto.
    + specialize (H0 n). specialize (H1 n).
      set (s1 := lcs eq_dec (a::l) l0) in *.
      set (s2 := lcs eq_dec l (a0::l0)) in *.
      destruct H0 as (H01 & H02 & H03).
      destruct H1 as (H11 & H12 & H13).
      cbn zeta.
      destruct (Nat.ltb_spec (length s1) (length s2)).
      * split; [|split].
        -- constructor. assumption.
        -- assumption.
        -- intros. inversion H1; subst.
           ++ apply Subseq_elim_cons_neq in H2; try assumption.
              specialize (H03 _ H1 H2). lia.
           ++ auto.
      * split; [|split].
        -- assumption.
        -- constructor. assumption.
        -- intros. inversion H1; subst.
           ++ apply Subseq_elim_cons_neq in H2; try assumption.
              specialize (H03 _ H1 H2). assumption.
           ++ rewrite <- H0. eauto.
Qed.

(This is my solution to https://www.codewars.com/kata/5de035e4b0285b002248ff7c.)

If I apply lcs_elim then everything works, but if I use instead intros; funelim (lcs eq_dec xs ys), the whole script works, but then the Qed fails. Moreover, apply lcs_elim is instantaneous, while funelim (lcs eq_dec xs ys) takes 0.5s, but I do not know whether this is expected.

[eponier]

Version 1.2.3 on Coq 8.12.

[mattam82]

My bugfix fixes the example of @eponier but probably not the one of @TheoWinterhalter