In the following simple theorem the proof is given directly in the form of a proof function. I'd like to understand how the two terms, parenthesized to reflect my concept, combine into a final proof function that returns the expected type.
Lemma simple : forall i, i <= S i.
Proof
fun i => (le_S i i) (le_n i).
It seems as if the (le_S i i) constructor term returned a function which then would accept (le_n i) as a parameter. Could someone be kind to explain how proof function combination works here?
You might want to read (https://en.wikipedia.org/wiki/Curry–Howard_correspondence).
Basically in Coq proofs are functions which take evidence (in form of a witness) for some proposition as arguments and produce evidence (a witness) for a new derived proposition.
If you do Check le_S. you get
le_S
: forall n m : nat, n <= m -> n <= S m
So le_S is a function which takes two nats and a witness for n <= m and produces a witness for n <= S m.
In you example le_n i is a witness for i <= i.
Please note that the ->symbol has the same meaning for usual functions like Check Nat.add.
Nat.add
: nat -> nat -> nat
as for proofs. a -> b in both cases means function from type a to type b.