0

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.

4

1 回答 1

2

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

于 2019-10-31T20:36:01.953 回答