Coq fight post-mortem

[Tony Sloane]

Thanks all for the Coq fight last night. Had a great time even though I didn’t come away with the trophy.

As expected, in the cool light of today away from the fighting arena, some lemmas that bamboozled last night were easily solved :-)

In case someone is interested in the T5 lemma that took too long to prove in the final round, I’ve included my proof below.

cheers,
Tony

(* T5 *)

Require Import Coq.Lists.List.

Definition justx (x : nat) (xs : list nat) :=
filter (fun y => beq_nat x y) xs.

Lemma empty_justx_not_in:
forall x xs,
justx x xs = nil -> ~ In x xs.
Proof.
unfold not. intros. induction xs.
(* nil *)
inversion H0.
(* cons *)
simpl in H.
remember (beq_nat x a) as eq. destruct eq.
(* true *)
inversion H.
(* false *)
inversion H0.
(* a = x *)
rewrite H1 in Heqeq.
rewrite <- beq_nat_refl in Heqeq.
inversion Heqeq.
(* In x xs *)
apply IHxs. apply H. apply H1.
Qed.

[Paul A. Steckler]

Sorry I couldn't attend the festivities.

But my money would've have been on Tony. :-)

-- Paul

> --
> You received this message because you are subscribed to the Google Groups "fp-syd" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to fp-syd+un...@googlegroups.com.
> To post to this group, send email to fp-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/fp-syd.
> For more options, visit https://groups.google.com/d/optout.

[Amos Robinson]

Yeah, I think beq_nat_refl was the missing piece of the puzzle.
It's just too hard to remember details of the standard library in that
high stress situation!
Amazing fun, and great commentary - I think it's definitely worth
doing again next year.

[Ben Lippmeier]

On 24 Apr 2014, at 10:56 , Paul A. Steckler <st...@stecksoft.com> wrote:

But my money would've have been on Tony. :-)

Then you would have lost it. :-)

I'll do a proper blog post with more photos over the weekend.

[Dom De Re]

Yep thanks all,

I had tonnes of fun on the night and in learning Coq in the lead up to the event.

Looking forward to the next one already!

[Chris Kohlhepp]

Can anyone advise if Coq can be used to verify / emit Lisp programs ?

Also, I am looking for something with which to verify the big-O of algorithms.

Can Coq be used to conduct such proofs ?

Thanks much

Chris Kohlhepp

[Dom De Re]

As far as I know, Coq cannot extract lisp, only Haskell, OCaml and Scheme.

As for proving the complexity of algorithms, it looks doable.  Google turns up some proofs for the complexity of various sorting algorithms and etc...

I don't know how much support there is for it in the standard library though.

You received this message because you are subscribed to a topic in the Google Groups "fp-syd" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/fp-syd/BjoSS9goHQ0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to fp-syd+un...@googlegroups.com.

[Chris Kohlhepp]

Thanks Dom

Scheme would be close enough for comfort. How did you find working with Coq?

Yu took part in the recent Coq fight, yes ?

Chris Kohlhepp

[Dom De Re]

Yeah I took part.

Working with Coq felt pretty natural.  It definitely felt better than having to write up Arbitrary instances.

But I hadn't done any proofs relating to complexity

I think verifying complexity of a function will require lemmas that describe how the cost of computations combine in different cases.  I dont know how many of these you would have to write yourself or how many already exist in the standard libs somewhere, if any.

[Chris Kohlhepp]

Hello Dom,

Thanks for the feedback

Best Regards

Chris Kohlhepp