Как переписать данные два зависимых типа равны в Coq

Question

Я работаю над доказательством, используя битовые векторы из библиотеки bbv , которые выглядят как word : nat -> Set. Я пытаюсь доказать, что самый старший бит остается тем же, если вы отрубите несколько младших битов:

Require Import bbv.Word.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Plus.

Lemma drop_msb : forall (n : nat) (x : word (S (S n))),
  wmsb x false = wmsb (wtl x) false.

Чтобы доказать это, следующая лемма кажется полезной:

Check wmsb_split2.
(*
wmsb_split2 :
  forall sz (w: word (sz + 1)) b,
    wmsb w b = if weq (split2 _ 1 w) (natToWord _ 0) then false else true.
*)

Вот моя попытка доказательства:

Proof.
  intros n x.
  assert (Snp : S (S n) = S n + 1). {
    rewrite <- Nat.add_1_l.
    apply plus_comm.
  }
  assert (xeq : word (S (S n)) = word ((S n) + 1)). {
    rewrite Snp.
    reflexivity.
  }
  rewrite wmsb_split2. (* Error: Found no subterm matching "wmsb ?M1864 ?M1865" in the current goal. *)

Вот состояние доказательства.

  n : nat
  x : word (S (S n))
  Snp : S (S n) = S n + 1
  xeq : word (S (S n)) = word (S n + 1)
  ============================
  wmsb x false = wmsb (wtl x) false

Я запутался, почему wmsb_split2 не может быть применено; Я вижу wmsb _ _ прямо в заключении! Нужна ли мне какая-то форма уникальности удостоверений личности, приведенных в EqDepFacts ?

У меня также есть дополнительные утверждения на случай, если мне нужно переписать x, но я не могу сделать что либо.

Answer 1

Существует более простое доказательство вычислением: поскольку word определяется как список битов, проиндексированных по его длине, если вы знаете, что длина равна S (S n), то первые два конструктора списка определяются однозначно, и этот факт обеспечивается леммой destruct_word_S.

destruct_word_S :
  forall (sz : nat) (w : word (S sz)),
    exists (v : word sz) (b : bool), w = WS b v

. В этом случае это позволяет дважды перезаписать x : word (S (S n)), в какой-то термин WS b0 (WS b1 x''), что включает как wmsb, так и wtl для вычисления.

Чтобы использовать destruct_word_S для переписывания, вы должны уничтожить два exists, чтобы получить равенство w = WS b v.

Lemma drop_msb : forall (n : nat) (x : word (S (S n))),
  wmsb x false = wmsb (wtl x) false.
Proof.
  intros.
  destruct (destruct_word_S x) as [x' [b0 Ex]].
  destruct (destruct_word_S x') as [x'' [b1 Ex']].
  rewrite Ex.
  rewrite Ex'. cbn.
  (* Goal: wmsb x'' b1 = wmsb x'' b1 *)
  reflexivity.
Qed.

---

Я запутался, почему wmsb_split2 не может быть применен; Я вижу wmsb _ _ прямо в заключении!

Длина слова является неявным аргументом для wmsb, и это то, что здесь не объединяет: лемма wmsb_split2 использует @wmsb (sz + 1) и ваша цель использует @wmsb (S (S n)) с левой стороны и @wmsb (S n) с правой стороны. Но sz + 1 не может быть преобразовано в S (S n) (т. Е. Они не могут нормализоваться к одному и тому же термину для любого экземпляра sz).

При работе с индексированными типами, такими как word, который индексируется по длине, равенство ведет себя совершенно неинтуитивно.

Я считаю, что в этом контексте хорошо работают принципы инверсии, такие как destruct_word_S, сформулированные в терминах однородного равенства, т.е. , = / eq, где обе стороны имеют один и тот же тип.

Напротив, гетерогенное равенство означает проблему, и это то, с чем вы сталкиваетесь, когда начинаете думать в терминах «word (S sz) - это тоже word (sz + 1)», пытаясь приравнять вещи разных типов.

К сожалению, я не знаю хорошего способа получить правильную интуицию здесь, кроме менее чем Удовлетворительный путь изучения теории зависимых типов: трактовать eq как «просто еще один индуктивный тип», осознавая, что он не ведет себя как наивная идея «равенства».