addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwchatcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-crosscrosseditemptyheartfacebookfolderfullheartglobegmailgoogleimagesinstagramlinklocation-pinmagnifying-glassmailminusmoremuplabelShape 3 + Rectangle 1outlookpersonplusprice-ribbonImported LayersImported LayersImported Layersshieldstartrashtriangle-downtriangle-uptwitteruseryahoo

Do the second chapter of Software Foundations: Induction

  • Apr 21, 2014 · 7:00 PM
  • Mixrank

Let's go through the exercises in the Induction chapter of SF, and then get together and discuss them.

Induction lets us prove some theorems that aren't totally trivial, so Coq starts to get a little more fun.

As I think we agreed this evening, interaction with Coq can be a little mysterious. Don't stress out! I suspect we're learning something even when we're just flailing around, so feel free to flail away. And post a message on meetup or the Google group if you get stuck on something.

Join or login to comment.

  • Fletcher Stump S.

    So I was able to find a proof that (fromUnary (toUnary z) = normalize z). It took about 10 lemmas, though they weren't too bad. I think the take away from all this is that, most of the time, the definitions will be too clumsy to prove anything non-trivial from. Developing a theory of the objects you are working with prior to set at to prove what you want to prove is essential. This is of course also true with traditional mathematics, but of course in practice most of the leg work has been done for us.

    Here is my code: https://github.com/fletcherdss/Coq-Exercises

    April 25, 2014

  • Christopher B.

    At probably a more elementary level, Scala Bay has a session May 12 on type-theoretic theorem proving with some intro to Coq. http://www.meetup.com/Scala-Bay/events/178469482/?a=ea1_grp&rv=ea1

    April 25, 2014

  • Sergei W.

    My verdict about the 5-star exercise in chapter 2: This exercise is hard, and there is no simple solution. Perhaps there is a non-elegant, long and complicated solution where you need to define twenty or so lemmas about various properties of all those functions (normalize, is_zero, etc.), and then you prove the theorem after many small steps. If you spend a week writing various lemmas and going forward in small steps, you might solve it. I wouldn't try.

    The give-away for me is that the authors give ample hints about relatively minor difficulties in other places, but here they give strictly no hints. My guess is that the authors also do not know any simple and short way to solve it, but they were too shy to say openly that the solution is long and ugly. It would be good to know if this is indeed the case.

    April 21, 2014

    • Adrian K.

      If the exercise had had two stars, then nat-to-bin-and-back-agai­n would have been the obvious answer. But putting 5 stars on it strongly suggested (to me at least) that that couldn't be the right answer. So, effectively, this question is hard mainly because it is *labeled* hard.

      April 23, 2014

    • Adrian K.

      I'd be a lot more impressed with what I've learned about Coq if I were able to prove that two distinct algorithms were equivalent. Proving an algorithm equivalent to itself (close enough) is a bit of a letdown.

      April 23, 2014

  • Sergei W.

    (* Examples.
    Absurdity involving only constants *)
    Example Absurdity_1 : true=false -> 10 = 5.
    Proof. apply ad_absurdum. Qed.

    (* Absurdity involving variables *)
    Example Absurdity_2 : forall (a b c : nat),
    true=false -> [a;b]=[b;c].
    Proof.
    intros a b c. (* need to introduce only the variables *)
    apply ad_absurdum.
    Qed.

    April 22, 2014

    • Sergei W.

      What exactly does this tactic do?

      April 22, 2014

    • Andrew B.

      Magic. Not really though. You can think about it as a much more powerful version of destruct. But instead of breaking down by case, it finds type constructors that fit whatever term you are inverting. So for some cases it may have the same effect as using destruct, but for the case illustrated above, it finds the only constructor that fits the term false=true which is the Prop False (This will be covered in later chapters) which immediately proves whatever you are doing since absurdity implies everything.

      April 22, 2014

  • Sergei W.

    (* How to prove anything from true=false? In classical logic, anything follows from a false statement. But Coq uses intuitionistic logic and cannot say that any statement is "false". So any derivation from true=false must be constructive and proceed like any other derivation. *)

    (* auxiliary function *)
    Definition const_b_map (T:Type)(f:bool)(a:T)(b:T) :=
    match f with
    | true => a
    | false => b
    end.

    (* main lemma *)
    Lemma ad_absurdum : forall (T : Type) (a b : T),
    true=false -> a=b.
    Proof.
    intros. (* goal: a=b *)
    assert (H1 : a = const_b_map T true a b).
    (*proof*) reflexivity. (* [] *)
    (* goal: a=b *)
    rewrite -> H1. (* goal: const_b_map T true a b = b *)
    rewrite -> H. (* goal: const_b_map T false a b = b *)
    reflexivity. Qed.

    April 22, 2014

  • Christopher B.

    Had been looking forward to this, but something came up and I unfortunately won't be able to attend this time.

    April 21, 2014

  • Sergei W.

    I started chapter 3 and hope to finish it soon... But so far I haven't been able to solve the hardest exercise in chapter 2, even with techniques of chapter 3.

    April 17, 2014

  • Ian Z.

    Definitely planning to come (and do the exercises before). Btw, I bought the Bertot/Casteran book and it is very helpful in seeing the larger picture.

    April 16, 2014

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy