Exercises sheet 2: Tactics and Proofs

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition fixme {T} : T. Admitted.

Exercise: prove that view (one branch is by induction)
Lemma all_filterP T a (s : seq T) :
  reflect (filter a s = s) (all a s).
Proof.
Admitted.

Exercise: prove using induction once more
Lemma mem_cat (T : eqType) (x : T) s1 s2 :
  (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
Proof.
Admitted.

Exercise: prove this by induction on s
Lemma allP (T : eqType) (a : pred T) (s : seq T) :
  reflect (∀ x, x \in s → a x) (all a s).
Proof.
apply: (iffP idP).
Admitted.

Exercise: prove the following lemma
Inductive form : Type :=
  | TT : form
  | FF : form
  | Not : form → form
  | And : form → form → form
  | Or : form → form → form.

Fixpoint evalfb (f : form) : bool :=
  match f with
  | TT ⇒ true
  | FF ⇒ false
  | Not f ⇒ ~~ (evalfb f)
  | And f1 f2 ⇒ evalfb f1 && evalfb f2
  | Or f1 f2 ⇒ evalfb f1 || evalfb f2
  end.

Fixpoint evalf (f : form) : Prop :=
  match f with
  | TT ⇒ True
  | FF ⇒ False
  | Not f ⇒ ¬ (evalf f)
  | And f1 f2 ⇒ evalf f1 ∧ evalf f2
  | Or f1 f2 ⇒ evalf f1 ∨ evalf f2
  end.

Lemma evalP f : reflect (evalf f) (evalfb f).
Proof.
apply: (iffP idP).
Admitted.

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

Section ListMonotonic.

Implicit Types (A B : eqType).

Lemma flatten_mon A B (l1 l2 : seq (seq A)) :
  {subset l1 ≤ l2} →
  {subset flatten l1 ≤ flatten l2}.
Admitted.

Lemma map_mon A B (f : A → B) l1 l2 :
  {subset l1 ≤ l2} →
  {subset [seq f i | i <- l1] ≤ [seq f i | i <- l2]}.
Admitted.

Lemma flatten_map_mon A B (f1 f2 : A → seq B) l1 l2:
  (∀ l, {subset f1 l ≤ f2 l}) →
  {subset l1 ≤ l2} →
  {subset flatten (map f1 l1) ≤ flatten (map f2 l2)}.
Admitted.

Lemma pmap_mon A B (f : A → option B) l1 l2 :
  {subset l1 ≤ l2} →
  {subset pmap f l1 ≤ pmap f l2}.
Admitted.

End ListMonotonic.

Section SetMonotonic.

Implicit Types (A B : finType).

Lemma imset_mon A B (f : A → B) (s1 s2 : {set A}) :
  s1 \subset s2 →
  [set f x1 | x1 in s1] \subset [set f x2 | x2 in s2].
Admitted.

End SetMonotonic.

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.
Section MiniLog.
Finitely-many literals.
Variable symbol : finType.
Variable domain : finType.
Variable ar : {ffun symbol → nat}.

Ground literals
Inductive lit := Lit : ∀ s : symbol, (ar s).-tuple domain → lit.

We 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.

Now you can read from here
Section Interp.

Interpretations are set of ground literals
Notation interp := ({set lit}).

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.
Variable (v : nat).
Inductive term :=
  | Val of domain
  | Var of 'I_v.

Inductive olit := OLit of ∀ s : symbol, (ar s).-tuple term → olit.
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:
Inductive clause := Clause of lit & seq lit.
Inductive oclause := OClause of olit & seq olit.
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) (ocl : oclause) (l : olit).

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.
Definition gr : finType := fixme.
You should be able to write now a function grounding a term, a literal, and clause:
Definition gr_term (s : gr) (t : term) : domain := fixme.
Definition gr_lit (s : gr) (l : olit) : lit := fixme.
Definition gr_clause (s : gr) (t : oclause) : clause := fixme.
Notation gr_head s ocl := (head (gr_clause s ocl)).
Notation gr_body s ocl := (body (gr_clause s ocl)).
You should be able to write now validity for open clauses using the [∀ ] form to quantify over the finite set of groundings.
Definition clause_true cl i :=
  all [fun x ⇒ x \in i] (body cl) ==> (head cl \in i).

Definition oclause_true ocl i : bool := fixme.

We can also profit from this fact to define (a very inefficient) version of forward chaining:
Definition fwd_ochain ocl i :=
  [set gr_head s ocl | s : gr & all (mem i) (gr_body s ocl)] :|: i.
Now prove the lemmas that were shown in the lesson, but for the new definition:
Section SomeSetTheory.

Variable (I : finType).
Implicit Types (s : {set I}) (f : {set I} → {set I}).

Definition monotone f := ∀ s1 s2, s1 \subset s2 → f s1 \subset f s2.

End SomeSetTheory.

Lemma fwd_ochain_mon ocl : monotone (fwd_ochain ocl).
Proof.
Admitted.

Lemma fwd_ochain_model ocl i : i = fwd_ochain ocl i → oclause_true ocl i.
Proof.
Admitted.

Lemma model_fwd_ochain ocl m : oclause_true ocl m → m = fwd_ochain ocl m.
Admitted.

Lemma fwd_ochainP ocl m : reflect (m = fwd_ochain ocl m) (oclause_true ocl m).
Proof.
by apply/(iffP idP); [exact: model_fwd_ochain | exact: fwd_ochain_model].
Qed.

Lemma fwd_ochain_psound ocl i m : oclause_true ocl m →
   i \subset m → fwd_ochain ocl i \subset m.
Proof.
Admitted.

Lemma fwd_ochain_complete ocl m : oclause_true ocl m →
  ∃ m', m' = fwd_ochain ocl m' ∧ oclause_true ocl m' ∧ m' \subset m.
Proof.
case/minset_exists⇒ m_min /minsetP [? ? ?].
by ∃ m_min; split; [exact: model_fwd_ochain|].
Qed.

Another interesting alternative for completeness is to prove that the intersection of any two models is a model.
Lemma modelI ocl m1 m2 : oclause_true ocl m1 → oclause_true ocl m2 →
                         oclause_true ocl (m1 :&: m2).
Proof.
Admitted.

End Interp.
End MiniLog.

Print Assumptions fwd_ochain_complete.