Моя задача — реализовать экземпляр типа равенства для типа данных seq. Для этого мне нужно создать функцию сравнения и доказательство того, что эта функция верна:
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.
Результат:
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)
Как избавиться от x' в обеих частях равенства: (x'::xs = x'::ys)?
Пробовал case: (x' :: xs = x' :: ys), не помогло.
apply/(iffP (IH ys)). by move=> ->. case. exact.Это хорошо или можно еще улучшить? 31.10.2019apply/(iffP (IH ys)); congruence.01.11.2019