Stream: Coq users

Topic: ✔ Simple Question on the structure of Coq

Jacob Salzberg (Oct 28 2022 at 18:41):

Hi all,

I'm currently reading Coq'Art and having a small amount of confusion on the following piece:
In Coq'Art, they show how STLC and coq tactics are related. They claim tactics transform the goals. I can see how this is true for intros (the app goal in reverse) and for assumption (looks just like the var rule in reverse) but I can't see how apply transforms the goals. apply seems to transform things in the current context instead, for example if you have

H: i <= i

then apply le_S in results in _H_ being modified, not the goal.

Moreover, it allows (?) building terms that are typed in the proof tree, but not actually objects in the context, right? So for example, if in the context you have

\x : A.y

and you also have

x : A

then you can deduce that ((\x.y) x) is TYPED A, but you can't necessarily deduce that it's in the context right? So are the hypotheses objects in the context, or are the hypotheses all objects thus far DERIVED from the context through the proof rules,

thanks.

Karl Palmskog (Oct 28 2022 at 18:43):

for the practical view of what Coq tactics really do, I recommend taking a look at this: https://github.com/aspiwack/tacengine/releases/download/v0.1-draft/tacengine.pdf

Notification Bot (Oct 28 2022 at 18:48):

Jacob Salzberg has marked this topic as resolved.

Gaëtan Gilbert (Oct 28 2022 at 18:59):

the context is the list of hypotheses, ie a list of names with types (and sometimes bodies)
it is part of the goal, with the other part called the conclusion
therefore modifying the hypotheses modifies the goal

we also say that terms are typed in a context (objects is too generic a name imo), this is not the same as being part of the context since terms are not hypotheses
a term can be formed from an hypothesis and this term is typed in the context which contains the hypothesis
the term and the hypothesis are not quite the same but they share the same syntax, disambiguated by the (textual, meta level) context
so for instance apply H in H' talks about the term H and the hypothesis H' and modifies the goal by modifying the type of the hypothesis H' in the context

Last updated: Oct 01 2023 at 19:01 UTC