Created
September 15, 2014 14:42
-
-
Save etosch/76f56c1114418339d6e0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import List. | |
Require Import EqNat. | |
Definition alist := list (nat * bool). | |
Fixpoint in_assignment n (a : alist) : Prop := | |
match a with | |
| nil => False | |
| (h,_)::t => if beq_nat n h | |
then True | |
else in_assignment n t | |
end. | |
Lemma in_empty : forall a, in_assignment a nil -> False. | |
intros; compute in H; apply H. | |
Qed. | |
Fixpoint find_assignment n (a : alist) : in_assignment n a -> bool := | |
match a with | |
| nil => fun pf => match (in_empty n) pf with end | |
| (h, tv)::t => if beq_nat h n | |
then fun _ => tv | |
else find_assignment n t | |
end. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
From @arjunguha: