Stream: Coq users

Topic: Get the head constant of the goal


view this post on Zulip Li-yao (Dec 10 2020 at 17:15):

How can I get the head of the goal?

Parameter head : nat -> nat -> Prop.
Goal forall x y, head x y.
Proof.
  let h := fail (* TODO *) in
  pattern h.
  (* Desired result:

      ============
      (fun h => forall x y, h x y) head
  *)

Bonus points for:

view this post on Zulip Kenji Maillard (Dec 10 2020 at 18:31):

That probably does not count as a solution, does it ?

Axiom foo : forall {A}, A.

Ltac t x k :=
  let x' := eval hnf in x in
  lazymatch x' with
  | forall x, @?h x => t (h foo) k
  | ?h _ => t h k
  end + k x.
Ltac k x := pattern x.
Ltac pattern_head :=
  lazymatch goal with
  | [ |- ?G ] => t G k
  end.

Parameter head : nat -> nat -> Prop.
Goal forall x y, head x y.
Proof.
  pattern_head.

view this post on Zulip Li-yao (Dec 10 2020 at 18:45):

the axiom makes me go "hmmmm" but that seems to work anyway?

view this post on Zulip Paolo Giarrusso (Dec 10 2020 at 18:46):

just add coqchk to your proof-checking workflow to show the axiom's not actually used by the proof :smiling_imp:

view this post on Zulip Paolo Giarrusso (Dec 10 2020 at 18:47):

(of course not an actually reasonable suggestion)

view this post on Zulip Gaëtan Gilbert (Dec 10 2020 at 18:48):

Why end + k x instead of | _ => k x end?

view this post on Zulip Gaëtan Gilbert (Dec 10 2020 at 18:50):

also you should check that the head isn't foo (for when the goal is forall P, P)

view this post on Zulip Kenji Maillard (Dec 10 2020 at 19:26):

Gaëtan Gilbert said:

Why end + k x instead of | _ => k x end?

Because I don't know how to write Ltac code, I'm juste launching in parallel an army of monkey and a deepmind instance and see who comes back first with something that looks like a solution

view this post on Zulip Kenji Maillard (Dec 10 2020 at 19:27):

Gaëtan Gilbert said:

also you should check that the head isn't foo (for when the goal is forall P, P)

I thought that foo might leak in the goal in more subtle ways (and so the check would be harder to implement) but now that you mention it that might be the only scenario to be considered...

view this post on Zulip Kenji Maillard (Dec 10 2020 at 19:28):

Li-yao said:

the axiom makes me go "hmmmm" but that seems to work anyway?

If you prefer, you can work in Exceptional Type Theory and use raise instead, the point is just to have a temporary global section

view this post on Zulip Yannick Forster (Dec 10 2020 at 20:23):

If the axiom is a problem you can always open a section when you want to use the tactic:

view this post on Zulip Yannick Forster (Dec 10 2020 at 20:23):

Class enable_head := { foo_var : forall {A}, A }.

Ltac t x k :=
  let x' := eval hnf in x in
  lazymatch x' with
  | forall x, @?h x => t (h (foo_var)) k
  | ?h _ => t h k
  end + k x.
Ltac k x := pattern x.
Ltac pattern_head :=
  lazymatch goal with
  | [ |- ?G ] => t G k
  end.

Section bla.
  Variable doesntoccur : enable_head.
  Axiom occurs : False.

  Parameter head : nat -> nat -> Prop.
  Lemma test : forall x y, head x y.
  Proof.
    pattern_head.
    destruct occurs.
  Qed.

End bla.

Check test.```

view this post on Zulip Yannick Forster (Dec 10 2020 at 20:25):

But I'm not sure that's really more clean...


Last updated: Feb 04 2023 at 21:02 UTC