Skip to content

Instantly share code, notes, and snippets.

@amutake

amutake/eqascii.v

Last active August 29, 2015 14:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save amutake/5bd069627f63da066bd3 to your computer and use it in GitHub Desktop.
Save amutake/5bd069627f63da066bd3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
eqascii.v
Require Import Coq.Strings.Ascii.
Require Import Ssreflect.ssreflect Ssreflect.eqtype Ssreflect.ssrbool.
Definition eqascii (a a' : ascii) : bool :=
match a, a' with
| Ascii b0 b1 b2 b3 b4 b5 b6 b7, Ascii b0' b1' b2' b3' b4' b5' b6' b7' =>
(b0 == b0') && (b1 == b1') && (b2 == b2') && (b3 == b3') &&
(b4 == b4') && (b5 == b5') && (b6 == b6') && (b7 == b7')
end.
Lemma eqasciiP : Equality.axiom eqascii.
Proof.
by do 18!case; constructor. (* 終わらない *)
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment