How the proof goals get generated?

[lancejpollard]

As a narrowing down of this question, I am starting to learn more about Coq tactics (like in this cheatsheet, or full index), which are the algorithms used to solve the goals in a proof as they are generated.

After looking at THEOREMS.md, it appears Kind does the same sort of thing (having goals, at least). Where is that code exactly that implements it? And at a high level, how does the algorithm work? Like, what is the input to the algorithm (the theorem, how is it actually modeled/structured in code), and how does the algorithm generate a goal? Wondering how this works in some detail so I know better how proof assistants work.

Then in addition to how the goals are generated, how are the goals solved? Like when in Coq you do refl or reflexivity or whatever it is, it says "Solves the goal if it is a trivial equality." How does it do these sorts of things? In Kind at least.

[atennapel]

(disclaimer: I don't know any Kind specifics, so I'm talking in generalities below)

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  ?a

Here, when the typechecker reaches ?a, the expected type is Bool.not(Bool.not(b)) == b and the only variable in scope is b of type Bool. So the goal is the expected type at the point of ?a and it will also show all the variables in scope, because those can be used to solve the goal.

We can see that this information is exactly what Kind prints:

Goal ?a:
With type: Bool.not(Bool.not(b)) == b
With context:
- b: Bool

So when a goal ?a is reached then it prints out the expected type at that point and all variables in scope (aka the context).

A goal can be solved by replacing the ?a with a term that has the expected type. For example refl is a term that has type x = x for any x. So if you have a goal that has the form t = t for some t then you can use refl to solve this, because it has the expected type.

In Coq there's another layer inbetween called Tactics. These are used to generate the term to fit in the goal holes.

Haskell has a similar feature called "Typed Holes": https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/typed-holes.html

[lancejpollard]

This is helpful information, thank you. I was hoping to go a little deeper, not necessarily into exactly how Kind does it, Coq would work as well or any proof assistant really. But I am looking for basically the data structures and implementation details of how it works pretty much, this is still pretty high level. Like, what algorithms is it using to figure out what variables are in scope (it has an accumulated list I guess), but what happens when you run a tactic or add a command of sorts in the proof step, how does it then resolve what the next goal is implementation-wise, if that makes sense?

[atennapel]

In Kind the goals are part of the AST. When you are type checking you are traversing the AST while keeping track of which variables are in scope. So when you reach a goal/hole you have the information available. The next goal is just the next hole you reach while traversing the AST.

I don't know how Coq tactics work, similarly I assume.

You can study https://github.com/AndrasKovacs/elaboration-zoo for one way to implement type checkers. Though it's good to read "Types and Programming Languages" first.