-
-
Save etosch/76f56c1114418339d6e0 to your computer and use it in GitHub Desktop.
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. |
And by manually you mean we would prove it as a lemma, right?
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.
@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."
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.
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.