/proofs

formal methods exercises

Primary LanguageCoqApache License 2.0Apache-2.0

proofs

Proofs of simple mathematical properties

  • binary.v Inductive proof that given binary to unary conversion holds for:
    • bin2nat(code + 1) ≡ bin2nat(code) + 1
  • pumping.v Proof of Pumping Lemma for regular expressions.

Better use with Emacs Proof General. my .emacs