Skip to content

Instantly share code, notes, and snippets.

@etosch

etosch/snippet.v

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

This comment has been minimized.

Copy link
Owner Author

@etosch 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

This comment has been minimized.

Copy link
Owner Author

@etosch 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

This comment has been minimized.

Copy link

@cibelemf 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

This comment has been minimized.

Copy link
Owner Author

@etosch 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

This comment has been minimized.

Copy link

@cibelemf cibelemf commented Sep 23, 2014

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

@etosch

This comment has been minimized.

Copy link
Owner Author

@etosch 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

This comment has been minimized.

Copy link
Owner Author

@etosch 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

This comment has been minimized.

Copy link
Owner Author

@etosch 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
You can’t perform that action at this time.