|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|
|else in_assignment n t|
|Lemma in_empty : forall a, in_assignment a nil -> False.|
|intros; compute in H; apply H.|
|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|
@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
I think what really needs to happen here is for there to somehow be a proof attached to show that
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.
@arjunguha @cibelemf : So I just defined a lemma like in my last comment, which I'll call
The term "find_assignment a t" has type "in_assignment_prop a t -> bool"
which doesn't really surprise me. So, I updated the lemma to be:
and in the recursive call I add sneak in
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."