exercises_2

Exercises sheet 2: Tactics and Proofs

From mathcomp Require Import all_ssreflect.

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

Exercise: prove the below using 'move:', 'move=>' and a final apply

Definition goal_reorder A B C (H : B → A → C) : A → B → C.
Proof. Admitted.

Exercise: write orC : or A B -> or B A

Definition orC A B : A ∧ B → B ∧ A := sorry.

Exercise: prove that orC (orC P) = P

Lemma orC_inv A B (p : A ∧ B) : orC (orC p) = p.
Proof. Admitted.

Exercise: prove

Lemma orbC p q : p || q = q || p.
Proof. Admitted.

Exercise:

look up the definition of iter
prove this statement by induction

Lemma iterSr A n (f : A → A) x : iter n.+1 f x = iter n f (f x).
Proof. Admitted.

Exercise:

look up the definition of iter (note there is an accumulator varying during recursion)
prove the following statement by induction

Lemma iter_predn m n : iter n predn m = m - n.
Proof. Admitted.

Exercise:

use only rewrite and by

use Search to find the relevant lemmas (all are good but for ltn_neqAle) or browse the online doc

proof sketch:

        m < n = ~~ (n <= m)
              = ~~ (n == m || n < m)
              = n != m && ~~ (n < m)
              = ...

Lemma ltn_neqAle m n : (m < n) = (m != n) && (m ≤ n).
Proof. Admitted.

Exercise:

which is the size of an empty sequence?
Use lemmas about size and filter

Lemma has_filter (T : eqType) a (s : seq T) : has a s = (filter a s != [::]).
Proof.
Admitted.

Exercise 6: prove that by induction

Lemma filter_all T a (s : seq T) : all a (filter a s).
Proof.
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: 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,etc...) lemmas.

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.