Stream: Equations devs & users

Topic: Equations renames hypothesis ???


view this post on Zulip Thomas Lamiaux (Sep 20 2024 at 02:39):

Am I dreaming or Equations is renaming my hypothesis H ???

From Equations Require Import Equations.

Inductive vec A : nat -> Type :=
  | vnil  : vec A 0
  | vcons : A -> forall (n : nat), vec A n -> vec A (S n).

Arguments vnil {_}.
Arguments vcons {_} _ _ _.

Equations vmap {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n :=
vmap f 0 vnil := vnil ;
vmap f (S n) (vcons a n v) := vcons (f a) n (vmap f n v).

Arguments vmap {_ _} _ {_} _.

Definition vmap_cong {A B n} (f f' : A -> B) (v : vec A n) :
  (forall a, f a = f' a) -> vmap f v = vmap f' v.
Proof.
  intros H. funelim (vmap f v); simp vmap.
  - reflexivity.
  - f_equal. easy. apply H.

view this post on Zulip Matthieu Sozeau (Sep 20 2024 at 07:41):

Probably because it generalizes it first and forgets that it should not use "H" to introduce the induction hypothesis because a later hypothesis to be introduced uses it


Last updated: Oct 13 2024 at 01:02 UTC