Упрощение выражения со списком равенства - PullRequest
Новая
       63

Упрощение выражения со списком равенства

0 голосов
/ 31 октября 2019

Моя задача - реализовать экземпляр типа равенства для типа данных 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 ':: xs = x' :: ys)?

Я пытался case: (x' :: xs = x' :: ys), но это не помогло.

1 Ответ

2 голосов
/ 31 октября 2019

(На тот случай, если вы не знаете, эта лемма уже доказана в библиотеке seq. Найдите eqseqP.)

Ключевым этапом при завершении доказательства является лемма iffP. : 

iffP : forall P Q b, reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.

Таким образом, вызывая apply/(iffP (IH ys)), мы уменьшаем текущую цель до доказательства того, что xs = ys -> x' :: xs = x' :: ys и x' :: xs = x' :: ys -> xs = ys. Вы можете выполнить обе подцели, применив тактику congruence.

...