lesson_2_2
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.
Once we have the basics of writing programs and proofs in Coq sorted out,
the next natural question is how to organize them.
As we saw at the end of the last lesson, types may have for example some common
property such as decidability of equality, or countability. So it'd be nice if we
could have a generic theory for these kind of types that we could use.
A good example is indeed equality, let's prove this statement about equality and natural numbers:
Lemma nat_eq_dec : ∀ (n m : nat), n = m ∨ n ≠ m.
Proof. Admitted.
Proof. Admitted.
This is a lemma that may need to use often, for example to reason about an indexing function.
However, we already have the eqn function that in a sense does exactly the same than the proof, and
moreover, it is faster to run. So we can maybe try to relate them with reflect?
Lemma nat_eqP n m : reflect (n = m) (eqn n m).
Proof. Admitted.
Proof. Admitted.
That looks quite good, now we can prove the previous lemma in a bit more convenient way:
Lemma nat_eq_dec' : ∀ (n m : nat), n = m ∨ n ≠ m.
Proof. Admitted.
Proof. Admitted.
But not only nat decidable equality, but many other types, and indeed,
we'd like to reason in our proof about when two things are equal.
While it is safe in Coq to add the excluded middle axiom, for some other properties of types
an axiom won't suffice. So we need a way to organize this, so what we do is to declare an interface
eqType for types with decidable equality:
Print eqType.
Print Equality.type.
Print Equality.mixin_of.
Print Equality.axiom.
Print Equality.type.
Print Equality.mixin_of.
Print Equality.axiom.
We did print the real thing as it is often convenient to see the not so rosy reality
of optimized libraries, but the above is basically implementing a mixin OO pattern, so
other structures can inherit efficiently from eqType.
Thanks to eqType we now have some interesting stuff. Let's do the proof again:
About eqP.
Lemma nat_eq_dec'' : ∀ (n m : nat), n = m ∨ n ≠ m.
Proof. Admitted.
Lemma nat_eq_dec'' : ∀ (n m : nat), n = m ∨ n ≠ m.
Proof. Admitted.
Note that there was a quite magic process in which Coq realized that nat
has an eqType instance. The mechanism implementing this is called "Canonical
Structures" and it is a form of inference that can be triggered by unification.
The implementation is a low level detail, and end-users have better tools this days, for
example "Hierarchy Builder" that will help them manage all these structures.
Other systems like Lean have built-in support (using type classes). Having eqType available allows us to
have some nice functions.
About undup.
Lemma size_dedup (T : eqType) (s : seq T) : size (undup s) ≤ size s.
Proof. Admitted.
Search _ list eqType.
Lemma mem_filter (T : eqType) (a : pred T) (x : T) (s : seq T) :
(x \in [seq x <- s | a x]) = a x && (x \in s).
Proof. Admitted.
Search _ list (mem _).
Lemma size_dedup (T : eqType) (s : seq T) : size (undup s) ≤ size s.
Proof. Admitted.
Search _ list eqType.
Lemma mem_filter (T : eqType) (a : pred T) (x : T) (s : seq T) :
(x \in [seq x <- s | a x]) = a x && (x \in s).
Proof. Admitted.
Search _ list (mem _).
That's great, and moreover math-comp provides facilities to build
class instances for isomorphic types. This saves a lot of time and
effort.
math-comp provides a very rich hierarchy or algebraic structures,
which we will explore soon. See
https://math-comp.github.io/htmldoc/libgraph.html
Let's explore that graph and the documentation a bit. Unfortunately not a very nice search.
Relevant classes at this stage are:
We end the lesson by developing a verified Datalog interpreter
step-by-step, in very few lines, thanks to the math-comp theory on
finite types (and a smart trick)
- eqType: types with decidable equality, operator ==, main theory eqP
- subType: types that meet a decidable (thus irrelevant) predicate
- choiceType: eqTypes with a choice principle, main theory xchoose, xchooseP
- countType: choiceTypes that are in bijection with the naturals, pickle, unpickle
- finType: countTypes that are finite, large theory of cardinality, decidable quantification, etc...
Section MiniLog.
Finitely-many literals.
Variable symbol : finType.
Variable domain : finType.
Variable ar : {ffun symbol → nat}.
Inductive lit := Lit : ∀ s : symbol, (ar s).-tuple domain → lit.
Variable domain : finType.
Variable ar : {ffun symbol → nat}.
Inductive lit := Lit : ∀ s : symbol, (ar s).-tuple domain → lit.
Build a finType instance for lit
Section LitFinType.
Notation max_ar := (\max_(s in symbol) ar s).
Lemma max_ar_bound y : ar y < max_ar.+1.
Proof. exact/leq_bigmax_cond. Qed.
Notation plit := ({x : 'I_(max_ar.+1) & (symbol × x.-tuple domain)%type}).
Definition lit_to_plit (l : lit) : plit :=
let: Lit s args := l in existT _ (Ordinal (max_ar_bound s)) (s, args).
Definition plit_to_lit (e : plit): option lit.
case: e ⇒ x [s]; case: (val x == ar s) / eqP ⇒ [-> | _] args;
[exact/Some/(Lit args)|exact/None].
Defined.
Lemma lit_to_plitK : pcancel lit_to_plit plit_to_lit.
Proof. by case⇒ [s args] /=; case: eqP ⇒ // ?; rewrite !eq_axiomK. Qed.
Canonical lit_eqType := Eval hnf in EqType lit (PcanEqMixin lit_to_plitK).
Canonical lit_choiceType := Eval hnf in ChoiceType lit (PcanChoiceMixin lit_to_plitK).
Canonical lit_countType := Eval hnf in CountType lit (PcanCountMixin lit_to_plitK).
Canonical lit_finType := Eval hnf in FinType lit (PcanFinMixin lit_to_plitK).
End LitFinType.
Notation max_ar := (\max_(s in symbol) ar s).
Lemma max_ar_bound y : ar y < max_ar.+1.
Proof. exact/leq_bigmax_cond. Qed.
Notation plit := ({x : 'I_(max_ar.+1) & (symbol × x.-tuple domain)%type}).
Definition lit_to_plit (l : lit) : plit :=
let: Lit s args := l in existT _ (Ordinal (max_ar_bound s)) (s, args).
Definition plit_to_lit (e : plit): option lit.
case: e ⇒ x [s]; case: (val x == ar s) / eqP ⇒ [-> | _] args;
[exact/Some/(Lit args)|exact/None].
Defined.
Lemma lit_to_plitK : pcancel lit_to_plit plit_to_lit.
Proof. by case⇒ [s args] /=; case: eqP ⇒ // ?; rewrite !eq_axiomK. Qed.
Canonical lit_eqType := Eval hnf in EqType lit (PcanEqMixin lit_to_plitK).
Canonical lit_choiceType := Eval hnf in ChoiceType lit (PcanChoiceMixin lit_to_plitK).
Canonical lit_countType := Eval hnf in CountType lit (PcanCountMixin lit_to_plitK).
Canonical lit_finType := Eval hnf in FinType lit (PcanFinMixin lit_to_plitK).
End LitFinType.
Now you can read from here
Section Exercise.
Interpretations are set of literals
Notation interp := ({set lit}).
A literal is true in i if it belongs (the negated version would be \isnot) Notation lit_true i l := (l \in i).
We define stupid clauses.
Inductive clause := Clause of lit & seq lit.
Definition head cl := let: Clause h b := cl in h.
Definition body cl := let: Clause h b := cl in b.
Implicit Types (i m : interp) (cl : clause) (l : lit).
Definition head cl := let: Clause h b := cl in h.
Definition body cl := let: Clause h b := cl in b.
Implicit Types (i m : interp) (cl : clause) (l : lit).
A clause is true.
Definition clause_true cl i :=
all (mem i) (body cl) ==> (head cl \in i).
all (mem i) (body cl) ==> (head cl \in i).
fwd chain is an interpretation transformer that takes a program and
a current interpretation and extends it with the new deducible facts.
Definition fwd_chain cl i := if all (mem i) (body cl) then (head cl) |: i else i.
Exercise 1 & 2: Prove the next two lemmas
- Hint: unfold and look for common parts in the defs!
- Hint: the proofs should be short and similar!
Lemma fwd_chain_model cl i : fwd_chain cl i = i → clause_true cl i.
Proof.
rewrite /fwd_chain /clause_true; case: ifP ⇒ // _.
by move/setUidPr; rewrite sub1set.
Qed.
Lemma model_fwd_chain cl m : clause_true cl m → fwd_chain cl m = m.
Proof.
rewrite /fwd_chain /clause_true; case: ifP ⇒ //= _ h.
by apply/setUidPr; rewrite sub1set.
Qed.
Lemma fwd_chainP cl m : reflect (fwd_chain cl m = m) (clause_true cl m).
Proof. by apply/(iffP idP);[exact: model_fwd_chain|exact: fwd_chain_model]. Qed.
Proof.
rewrite /fwd_chain /clause_true; case: ifP ⇒ // _.
by move/setUidPr; rewrite sub1set.
Qed.
Lemma model_fwd_chain cl m : clause_true cl m → fwd_chain cl m = m.
Proof.
rewrite /fwd_chain /clause_true; case: ifP ⇒ //= _ h.
by apply/setUidPr; rewrite sub1set.
Qed.
Lemma fwd_chainP cl m : reflect (fwd_chain cl m = m) (clause_true cl m).
Proof. by apply/(iffP idP);[exact: model_fwd_chain|exact: fwd_chain_model]. Qed.
if the program p has a model m
then fwd_chain has a fixpoint m' s.t m' is a model for p
and a better or equal model than m
Lemma fwd_chain_complete cl m : clause_true cl m →
∃ m', fwd_chain cl m' = m' ∧ clause_true cl m' ∧ m' \subset m.
Proof.
case/minset_exists⇒ m_min /minsetP [? ? ?].
by ∃ m_min; split; [exact: model_fwd_chain|].
Qed.
Section MiniLog.
Print Assumptions fwd_chain_complete.
∃ m', fwd_chain cl m' = m' ∧ clause_true cl m' ∧ m' \subset m.
Proof.
case/minset_exists⇒ m_min /minsetP [? ? ?].
by ∃ m_min; split; [exact: model_fwd_chain|].
Qed.
Section MiniLog.
Print Assumptions fwd_chain_complete.