Gallina := terms + vernacular Q: what's the difference between vernacular commands and Gallina vernacular? # Vernacular https://coq.inria.fr/refman/language/gallina-specification-language.html#the-vernacular Vernacular is the command language of Galina. Mostly centered on modifying (Assumptions, Definitions, Assertions) and querying the environment (Vernacular commands). ## Basic query commands - interact with the system - `Print term` -> prints the term ( - `Check term` -> ensures the term type checks the term's type - ... https://coq.inria.fr/refman/proof-engine/vernacular-commands.html ## Definitions https://coq.inria.fr/refman/language/gallina-specification-language.html#definitions `Definition ident := term` and other variations binds ident to term in the environment after type checking. ## Assertions https://coq.inria.fr/refman/language/gallina-specification-language.html#assertions Assertions state a type whose inhabitants are (interactively) built using tactics. Asserting a statement (typically `Theorem term`) enters proof editing mode. `Goal form` will also enter proof editing mode. `Theorem` (Lemma Fact Proposittion Remark Corollary are just synonyms) - https://coq.inria.fr/refman/language/gallina-specification-language.html#coq:cmd.theorem `Qed` extracts a proof term from the proof script, defines the original ident to have that term as a proof witness. "The name is added to the environment as an opaque constant." `Definition ident : type` Like `Theorem` but where the computational content matters. Closed with `Defined` instead of `Qed`, which binds the name transparently in the environment. - Basically like a `Definition ident := term` but where you don't want to write out the program manually but rather want to use tactics. ## Assumptions Similar to assertions but allows omitting the definied term. Extend the environment with axioms, parameters, hypotheses or variables. - Q: what's the difference between `Theorem` and `Definition` - They're the same, I think by convention, definitions are given directly while theorems are written using proof tactics - e.g. try to `Definition` a term with just a type sig and not body -> tyou enter a goal state. - `Goal term` manually enters a goal proving state - `Parameter term` manually creates a goal premise? - `Locate "op"` to figure out what custom syntax maps to. - e.g. `Locate "/\".` `"A /\ B" := and A B : type_scope...` # Terms ## Special syntax - `t1 = t2` infix syntax is rewritten to the Galina term `eq` ``` Print eq. Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x (* For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: Arguments A, x are implicit and maximally inserted For eq_refl, when applied to 1 argument: Argument A is implicit For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] *) ``` # Tactics Good overview of important tactics and proof approaches https://pjreddie.com/coq-tactics/#unfold Tactics automate proofs by generating proof witnesses / programs. Tactic scripts generate programs that satisfy the current proof goal (ie. a program of the correct type). Writing tactic scripts is assisted along the type-structure from gaols to subgoals (i.e. problems of decreasing size). Automatic generation of tactic scripts is equivalent to automated proof search and in the general case undecidable. (Many simpler theorems can be exhaustively proved with a with heuristic rules). ## Basic tactics - most basic tactics allow "computing" the terms along specific redexes (Beta, Eta...) - `simpl, eval, compute` - Q: which one does which redex? `simpl` seems to be most frequently used - Apply ? how does this work