2
$\begingroup$

I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use the coq notation (It must be galina) to write lambda functions, such as (fun x:Z => x+ 1) which map (x+1) to x. (I use this notation because I don't know what is the general one). "nat" is the type of natural integers.

Let's consider I have a theorem that involve a lambda function (For example (fun x:nat => x+n) and n is any natural, defined in an hypothesis of the lemma) Let's suppose the theorem work directly on the lambda function (I'm probably using inappropriate words o.o), like for example (It is wrong, but I just use this example for the example) : the sum of any two lambda functions (that both return a natural) equals 0.

My question is : is it possible (I mean, strictly formally) to use an external lemma that would for example say $\forall a, b \in \mathbb{N}, a + b = 2$ (I know this is completely wrong, but it is just for the example).
So is it possible to use this lemma in the first theorem I have stated, to rewrite $x + n$ into $2$, according to the lemma.

I am asking this question for two reasons : I have almost no experience with lambda-calculus, and I am not sure at all about the variable decalarations ...

(The subject's title might not be appropriate .. I apologize if it is the case)

Thanks in advance !

$\endgroup$
  • $\begingroup$ I think that's a matter of definition. In Coq, for example, theorems that are already proved are part of the current environment and can be used in later arguments. $\endgroup$ – Hanno Nov 13 '14 at 22:31
  • $\begingroup$ The problem in coq is that I can only rewrite in lambdas that can be beta-reduced (I mean, a lambda function that "does not have any arguments"). I don't really know how to say it otherwise .. $\endgroup$ – QuanticPotato Nov 13 '14 at 22:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.