rss.rst

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.


Lemma rev_rev {A} (l: list A) : List.rev (List.rev l) = l.
Proof.
  induction l; cbn.A:Type
nil = nil
A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (rev l ++ a :: nil) = a :: l
  - (* l ← [] *)A:Type
nil = nil
    reflexivity.

  - (* l ← _ :: _ *)A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (rev l ++ a :: nil) = a :: l
    rewrite rev_app_distr.rev (a :: nil) ++ rev (rev l) = a :: l
    rewrite IHl.rev (a :: nil) ++ l = a :: l
    cbn.a :: l = a :: l
    reflexivity.
Qed.