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)

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

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

just add `coqchk`

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

(of course not an actually reasonable suggestion)

Why `end + k x`

instead of `| _ => k x end`

?

also you should check that the head isn't `foo`

(for when the goal is `forall P, P`

)

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

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

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

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

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

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

Last updated: Jun 25 2024 at 15:02 UTC