Stream: Coq users

Topic: Ltac patten match on fixpoints


view this post on Zulip Lef Ioannidis (Apr 04 2023 at 17:08):

Hi in the following reproducible example I get the error
"struct" annotation is expected.
I don't know what Ltac expects exactly, how would you match on a fixpoint like that?

  Definition foo : nat -> Prop :=
    fix F n :=
      match n with
      | 0 => True
      | S n => False /\ F n
      end.

  Goal forall n, ~ foo (S n).
    intros.
    intro CONTRA.
    unfold foo in CONTRA.
    Fail match type of CONTRA with
    | context[((fix F : nat -> Prop := _) ?n)] => idtac F
    end.
  Admitted.

view this post on Zulip Kenji Maillard (Apr 04 2023 at 17:26):

fix (and Fixpoint) maintain the information of which argument they are structurally recursive on through a {struct n} clause, and that's what Ltac seems to be asking you :

    match type of CONTRA with
    | context[((fix F (x : nat) {struct x} : Prop := _) ?n)] => idtac F
    end.

view this post on Zulip Lef Ioannidis (Apr 04 2023 at 17:42):

Yes, that's exactly right. Thanks!


Last updated: Jun 18 2024 at 21:01 UTC