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. |
From @arjunguha:
Set Implicit Arguments.
Require Import List.
Require Import EqNat.
Require Import Coq.Arith.Peano_dec.
Definition alist := list (nat * bool).
Fixpoint in_assignment n (a : alist) : Prop :=
match a with
| nil => False
| (h,_)::t => match eq_nat_dec n h with
| left _ => True
| right _ => in_assignment n t
end
end.
Lemma in_empty : forall a, in_assignment a nil -> False.
intros; compute in H; apply H.
Qed.
Lemma helper : forall (n k : nat) (v : bool) (lst : list (nat * bool)),
in_assignment n ((k,v)::lst) ->
n <> k ->
in_assignment n lst.
Proof with auto using list.
intros.
induction lst.
+ simpl in H.
destruct (eq_nat_dec n k); contradiction.
+ simpl in H.
destruct (eq_nat_dec n k); try contradiction.
destruct a as [k1 v1].
destruct (eq_nat_dec n k1).
- subst. simpl. destruct (eq_nat_dec k1 k1). auto. unfold not in n. contradiction n...
- simpl in IHlst.
destruct (eq_nat_dec n k).
* subst. unfold not in H0. contradiction H0...
* simpl.
destruct (eq_nat_dec n k1). subst. unfold not in n1. contradiction n1... trivial.
Qed.
Fixpoint find_assignment n (a : alist) { struct a }: in_assignment n a -> bool.
refine (match a with
| nil => _
| (h,tv)::t =>
match eq_nat_dec n h with
| left eq_proof => fun _ => tv
| right neq_proof => fun pf => find_assignment n t (@helper n h tv t pf neq_proof)
end
end).
Proof.
+ intros.
apply in_empty in H.
inversion H.
Qed.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
@arjunguha @cibelemf : So I just defined a lemma like in my last comment, which I'll call
my_lemma
and rewrite the recursive call so it readselse my_lemma n t (h,tv) (find_assignment n t)
. This gave me the errorThe term "find_assignment a t" has type "in_assignment_prop a t -> bool"
while it is expected to have type "in_assignment_prop a t"
which doesn't really surprise me. So, I updated the lemma to be:
Lemma my_lemma: forall n t h tv P, in_assignment n t -> P -> (in_assignment n (h,tv):t -> P).
and in the recursive call I add sneak in
bool
as the penultimate argument tomy_fun
. Now the error I get is:The term "find_assignment a t" has type "in_assignment_prop a t -> bool" while it is expected to have type "in_assignment n t".
And now I'm stuck again.
NOTE: My lemma is unproven -- I just made it "Admitted."