Stream: Coq users

Topic: Get the head constant of the goal

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:

• not using intros (this is easy with intros, but, just as a matter of principle, can you do it without touching the generated Gallina term?)
• using Ltac1 (Ltac2 most likely makes this easy too, but 1: I would like to not get locked into 8.12, and 2: I'm currently stuck on the fact that Ltac1 match seems to only accept well-typed terms, and I'm wondering what workaround there are)

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.

Li-yao (Dec 10 2020 at 18:45):

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

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:

Paolo Giarrusso (Dec 10 2020 at 18:47):

(of course not an actually reasonable suggestion)

Gaëtan Gilbert (Dec 10 2020 at 18:48):

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

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)

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

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...

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

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:

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.```

Yannick Forster (Dec 10 2020 at 20:25):

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

Last updated: Oct 13 2024 at 01:02 UTC