a thoughtful web.
Good ideas and conversation. No ads, no tracking.   Login or Take a Tour!
ilex  ·  1099 days ago  ·  link  ·    ·  parent  ·  post: Proving the relationship between the golden ratio and the Fibonnaci numbers in Coq

I don't think coq is intuitive to anyone :) It might have the steepest learning curve of any language I've learned, possibly tied with Idris, which just so happens to be another dependently typed language.

The bits between Lemma and QED are kinda neat -- they're "proof tactics" written in the tactic language LTAC. It's kind of a metalanguage that directs Coq through synthesizing an actual program.

Like, for example, here's a simple proposition written in LTAC:

  Lemma fst : forall a b, a /\ b -> a.

intros a b [Ha Hb].

exact Ha.


and here's what Coq synthesizes for that:

  fst = 

fun (a b : Prop) (H : a /\ b) => match H with

| conj Ha _ => Ha


: forall a b : Prop, a /\ b -> a

(fun is the keyword for lambdas, kinda like \ in Haskell.)

In other words, that stuff is both program and proof!