My task is to implement an instance of equality type for the seq datatype. To do this I need to create a comparison function and a proof that this function is correct:
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Fixpoint eq_seq {T: eqType} (x y: seq T) : bool :=
match x, y with
| [::],[::] => true
| cons x' xs, [::] => false
| [::], cons y' ys => false
| cons x' xs, cons y' ys => (x' == y') && eq_seq xs ys
end.
Arguments eq_seq T x y : simpl nomatch.
Lemma eq_seq_correct : forall T: eqType, Equality.axiom (@eq_seq T).
Proof.
move=> T x. elim: x=> [|x' xs].
- move=> y. case: y=> //=; by constructor.
- move=> IH y. case: y=> [| y' ys].
+ rewrite /(eq_seq (x' :: xs) [::]). constructor. done.
+ move=> /=. case E: (x' == y').
* move: E. case: eqP=> E _ //=. rewrite <- E.
Result:
2 subgoals (ID 290)
T : eqType
x' : T
xs : seq T
IH : forall y : seq T, reflect (xs = y) (eq_seq xs y)
y' : T
ys : seq T
E : x' = y'
============================
reflect (x' :: xs = x' :: ys) (eq_seq xs ys)
subgoal 2 (ID 199) is:
reflect (x' :: xs = y' :: ys) (false && eq_seq xs ys)
How to get rid of x' in both sides of equality: (x' :: xs = x' :: ys)?
I tried case: (x' :: xs = x' :: ys), but it didn't help.
(Just in case you are not aware, this lemma is already proved in the seq library. Look for eqseqP.)
The key step in completing the proof is the iffP lemma:
iffP : forall P Q b, reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
Thus, by calling apply/(iffP (IH ys)), we reduce the current goal to proving that xs = ys -> x' :: xs = x' :: ys and x' :: xs = x' :: ys -> xs = ys. You can discharge both subgoals by applying the congruence tactic.