{{ message }}

Instantly share code, notes, and snippets.

# etosch/snippet.v

Created Sep 15, 2014
 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.

### etosch commented Sep 17, 2014

 @arjunguha do you think the issue is that it's "illegal" for me to re-bind the premises in the return type? I tried expressing this using the sig type and got a very similar message. In that case, the match is on a witness and a proof. The signature of find_assignment looks like `find_assignment n (a : { x : alist | in_assignment n x}) -> bool`. The recursive call cannot use the proof from the previous call. I need a new proof, but I'm not sure how to construct one.

### etosch commented Sep 23, 2014

 I think what really needs to happen here is for there to somehow be a proof attached to show that `in_assignment n t -> bool` implies `in_assignment n (h, tv)::t -> bool`. The more I think about it, the more I think that, even though I "know" the individual pieces to be true, Coq doesn't, nor should it.

### cibelemf commented Sep 23, 2014

 But this is a weird thing. How come Coq doesn't know the inductive structure? We can use them just fine in other proofs

### etosch commented Sep 23, 2014

 It can't remember the structure from the match statements. Apparently there are good reasons for this -- this kind of higher order inference is undecidable in the general case, and they don't want to hard-code heuristics for easy, specific cases. There might be a way to do with the "return" statement in the the match statement (e.g. `match a return in_assignment n a -> bool with`), but I'm not so sure now. The more I think about it, the more I'm convinced that in a case like this, we would need to manually provide proof that the one signature follows from the other.

### cibelemf commented Sep 23, 2014

 And by manually you mean we would prove it as a lemma, right?

### etosch commented Sep 23, 2014

 Yeah, I think so. I'm thinking something like this: we'd prove `forall n t h tv, in_assignment n t -> in_assignment n (h, tv)::t` and then would do something like call apply in the recursive call. It's weird.

### etosch commented Sep 24, 2014

 @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 reads `else my_lemma n t (h,tv) (find_assignment n t)`. This gave me the error The 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 to `my_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."

### etosch commented Dec 29, 2014

 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. ``````