Exercises sheet 2: Tactics and Proofs

Exercise: prove that view (one branch is by induction)
Exercise: prove using induction once more
Exercise: prove this by induction on s
Exercise: prove the following lemma
Exercise: Prove the following monotonicity lemmas.
No induction is allowed!
Hint: use the *P (mapP, flattenP, etc...) lemmas. Hint: recall that {subset l1 l2} is notation for x, x \in l1 x \in l2

Datalog Interpreter, with variables.

In the lesson, we saw a very simple Datalog interpeter for ground clauses. Your task now is to extend the interpreter so we can have variables in the clauses. In order to achieve that, we create a new type of terms that can contain variables, and use them in our literals.
Your job is to finish adapting the definitions, read below for more instructions.
Finitely-many literals.
Ground literals
We build a finType instance for lit
Now you can read from here
Interpretations are set of ground literals
A literal is true in i if it belongs (the negated version would be \isnot) We could use notation lit_true i l := (l \in i).
However, now our clauses can contain literals with variables. We define a term type.
Note that we can equip olit with all the instances for classes that we would need. Do so if needed in the exercise.
Using the new open literals, we define clauses:

Validity of clauses:

Our old definition clause_true < Definition clause_true cl i := all fun x x \in i (body cl) ==> (head cl \in i). >>> is not going to work now, as the literals in the body are not grounded anymore, thus Coq will complain about not being able to unify the types.
The new definition of clause validity is, informally "forall all groundings of the clause, the clause is interpreted to true in i."
Your first job will be to define a grounding using the {ffun T -> U} mathcomp construction. Remove the finType below, which is just to make the document work.
You should be able to write now a function grounding a term, a literal, and clause:
You should be able to write now validity for open clauses using the [ ] form to quantify over the finite set of groundings.
We can also profit from this fact to define (a very inefficient) version of forward chaining:
Now prove the lemmas that were shown in the lesson, but for the new definition:
Another interesting alternative for completeness is to prove that the intersection of any two models is a model.
Goals

Help
Messages