## 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.
lazymatch goal with
| [ |- ?G ] => t G k
end.

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

#### 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.
lazymatch goal with
| [ |- ?G ] => t G k
end.

Section bla.
Axiom occurs : False.

Parameter head : nat -> nat -> Prop.
Lemma test : forall x y, head x y.
Proof.
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: Jun 25 2024 at 15:02 UTC