получить поле из типов записей в Coq

Я новичок в Коке. У меня есть тип записи и одно определение:

Record t : Type := T {
  width           : nat;
}.

Definition indent shift f :=
  match f with
  | T w => T
    (w + shift)
  end.

Я хочу доказать тривиальную лемму:

Lemma lemma :
  forall (a:t) n, width a <= width (indent n a).

после развертывания indent подцель становится:

(width a <= width match a with
                   | {| width := w |} => {| width := w + n |}
                   end)

Как упростить термин?


coq coqide coq-tactic
person he11boy    schedule 29.12.2019    source источник

Ответы (3)


arrow_upward
0
arrow_downward

уничтожить а. простой

После этой индукции.

person he11boy    schedule 29.12.2019
comment
Использование induction здесь неверно; следует использовать лемму Nat.le_add_r или, в худшем случае, вызвать какую-либо арифметическую процедуру. - person ejgallego; 29.12.2019

arrow_upward
0
arrow_downward

Используйте другое определение, и simpl сделает всю работу:

Definition indent shift f := T (f.(width) + shift).
person ejgallego    schedule 29.12.2019

arrow_upward
0
arrow_downward

Когда вы видите термин с match a with ... end в нем, вы можете упростить его, выполнив destruct a. Также, если вам нужно избавиться от let a := b in .... Если вам нужно вспомнить, что такое a, сделайте destruct a eqn:Ha.

person larsr    schedule 30.12.2019