Skip to content

Instantly share code, notes, and snippets.

@etosch
Created September 15, 2014 14:42
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Embed
What would you like to do?
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
Copy link
Author

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
Copy link
Author

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
Copy link

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
Copy link
Author

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
Copy link

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

@etosch
Copy link
Author

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
Copy link
Author

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
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment