Skip to content

Instantly share code, notes, and snippets.

@jldodds

jldodds/gist:972091d6c2ad9597e83d

Created January 16, 2015 18:32
Show Gist options
  • Save jldodds/972091d6c2ad9597e83d to your computer and use it in GitHub Desktop.
Save jldodds/972091d6c2ad9597e83d to your computer and use it in GitHub Desktop.
Download ZIP
Simplifying sem_add_default
Raw
gistfile1.coq
Require Import floyd.proofauto
Goal forall a b, is_int I32 Signed a -> is_int I32 Signed b ->
exists i i1, sem_add_default tint tint a b = Some (Vint (Int.add i i1)).
intros. destruct a; try solve [inversion H].
destruct b; try solve [inversion H0].
unfold sem_add_default. simpl. unfold both_int. simpl.
eauto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment