coq - get field from Record Types in Coq

Question

I am new to Coq. I have a record type and one definition:

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

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

I want to proof a trivial lemma:

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

after unfolding indent subgoal becomes:

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

How to simplify term?

Answer 1

使用不同的定义simpl并将完成工作：

Definition indent shift f := T (f.(width) + shift).

Answer 2

破坏 a. 简单。

在那个感应之后。

Answer 3

当你看到一个带有match a with ... endin 的术语时，你可以通过做 来简化它destruct a。另外，如果您需要摆脱 let a := b in ... 如果您需要记住a曾经发生过的事情，请执行destruct a eqn:Ha.