# Tag Info

24

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own). Here is an example: ...

20

You're exactly right that the halting problem is an example of the second kind of "proof by contradiction" - it's really just a negative statement. Suppose decides_halt(M) is a predicate that says that machine M decides if its input is a machine that halts (that is, M is a program that for some machine m and input i, decides if m halts on input i). ...

15

Gilles answer is a good one, except for the paragraph on the real numbers, which is completely false, except for the fact that the real numbers are indeed a different kettle of fish. Because this sort of misinformation seems to be quite widespread, I would like to record here a detailed rebuttal. It is not true that all inductive types are denumerable. For ...

14

You cannot prove it in "vanilla" Coq, because it is based on intuitionistic logic: From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not valid logical rules. There are several ways you can deal with a situation like this. Introduce the law ...

14

Coq has 3 "big" types: Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$. This allows terms that are only used for proof to be erased in any code generated by Coq. Set is meant for computation. It's ...

12

There are multiple ways to define a mathematical structure, depending on what properties you consider to be the definition. Between equivalent characterizations, which one you take to be the definition and which one you take to be an alternative characterization is not important. In constructive mathematics, it is preferable to pick a definition that makes ...

12

What is second order logic in contrast to first order logic? What is monadic vs non monadic logic? Monadic second-order logic is first-order logic plus quantification over sets. So, as well as being able to say that there exists a domain element with some property ($\exists x\dots$), you can also say that there exists a set of domain elements with some ...

11

This is a very active research topic, very promising, though full automation of program generation probably has intrinsic limitations (but are human beings any better?). But the idea is still be very useful in assisting considerably the creation of programs by mechanizing many steps, and by automatically checking the correctness of the program generation. ...

9

I agree with you. There's a bijection between baz and False. Definition injective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1 x2, f1 x1 = f1 x2 -> x1 = x2. Definition surjective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1, exists x2, f1 x2 = x1. Definition bijective : forall {t1 t2}, (t1 -&...

9

The wag answer: Yes, but at the time of writing, for most nontrivial programs the specifications seem to be just as hard to write and debug as the programs would be. More seriously, babou's answer is good, but I'm also going to suggest checking out the area of dependent types. There's a rather good book using Coq (full disclaimer: written by a friend of ...

9

Inductive types are similar to Haskell's data, but they are more general. An inductive definition in Set describes a way to build a piece of data from smaller pieces. For example, the following definition defines a type called prod which allows taking two pieces of data and bundling them together. Inductive prod (A B : Set) : Set := pair : A -> B -> ...

8

When you do an existential introduction, you are saying there is some term $t$, which is represented by the unification variable ?x, such that $P(t)\to Q$. You then try to apply $P(t)$ to $H : (\forall x.P(x)) \to Q$. It tries to generalize P ?x, because if it can show that $P(c)$ for a fresh constant $c$ (represented by x in the Coq output), then $\forall x.... 8 You can ask Coq to show you its proof object. Before Qed, type Show Proof. (fun (_ : forall n : nat, evenb n = true -> oddb (S n) = true) (H2 : oddb 3 = true) => H2) As you can see, H1 is not used at all, and the goal is H2. It comes from the definition of oddb and evenb, the definition of negb and the definition of the natural numbers and the ... 7 Coq is a bit more cruel than paper proofs: when you write "and we are done" or "clearly" in a paper proof, there is often much more to do to convince Coq. Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here. Several remarks: I used built in datatypes and definitions where I thought it wouldn't hurt ... 7 it looks like we are assuming l2 doesn't change in the induction case. But when we later apply it with l2:=l1, we are breaking this assumption. No. If we regard l1 to be a value which is repeatedly decreased in the induction proof, note that we let l2 to be equal to the initial value of l1 -- such value will not change in the induction steps. In other ... 7 I'm not an expert, but I'll share what I understood so far with an example. Let's consider the boolean type in CoC, using its standard encoding: $$\begin{array}{l} \mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau \\ \mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x \\ \mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y \end{array}$$ We might expect to be able to ... 7 You can destruct not only on variables, but on expressions like f n as well. So, this will get you a solution: Lemma foo : forall n, f n = (let (x, y) := f n in (x, y)). intro n. now destruct (f n). (* or destruct (f n). reflexivity. *) Qed. 6 (1) We are just using this general theorem to prove a special case, we don't change anything here. When we use this coq construction apply app_length_cons' with (l1:=l1) (l2:=l1). we just in some sense instantiate this universally quantified formula $$\forall l_1, l_2. \mid l_1 \cdot (x :: l_2) \mid~=~succ \mid l_1 \cdot l_2 \mid$$ with$l_2 = l_1$:$...

6

As others informed you, your tautology is not a tautology unless you assume classical logic. But since you're doing tautologies on decidable truth values, you could use bool instead of Prop. Then your tautology holds: Require Import Bool. Lemma how_about_bool: forall (p : bool), Is_true (p || negb p). Proof. now intros [|]. Qed.

6

You are making your life difficult by defining things in convoluted ways. Here's how a better definition of the same thing makes the proof easy. Fixpoint f_better n0 len : Prop := match len with | 0 => True | S k => x n0 /\ f_better (S n0) k end. Theorem t1_better: forall n0 len, x n0 /\ f_better (S n0) len <-> f_better n0 (S len). ...

6

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest you start with Software Foundations. Most of your questions would be answered there. But, basically: Definition and Fixpoint are like OCaml's let and let rec,...

6

The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a proposition. One way to understand the differences between different conceptions of propositions-as-types is to view them as capturing different notions of provability ...

5

relational databases are among the highest value, most researched applications of computer science James, what do relational databases have to do with the question? And why have you tagged this q with 'relational-algebra'? It seems to me entirely gratuitous. Just because databases are 'relational' does not mean they have much to do with whatever Russell ...

5

You could also consider a more equational proof that will avoid/encapsulate the destruction: Lemma foo n : f n = (let (x, y) := f n in (x, y)). Proof. now rewrite (surjective_pairing (f n)). Qed.

5

to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z No, you can't prove that T Z = Z because it is false: Lemma TZ_neq_Z : T Z <> Z. Proof. discriminate. Qed. Indeed, distinct constructors of an inductive type always lead to distinct terms. That doesn't mean you can't prove that bin_to_nat is the inverse of ...

5

The positivity condition is not there just so that "programs terminate", as you put it (what programs?), but to make sure the type is well defined in the first place. The inductive definitions define the smallest type satisfying an equation. That is, we put into the type only those things which are prescribed by the clauses of the definition, and no ...

5

Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal. Most of the time, people doing maths are not exposed to mathematical logic. They do not know, for instance, how to define the set of real numbers. Or even the set of natural numbers. Numeric sets are ...

5

As the others have mentioned, in Coq's standard library (or typical presentations of naturals in Coq), naturals are defined inductively, usually a la Peano. We could make other choices, e.g. one could imagine defining naturals as the free semiring on one generator which would give you many of the "axiomatic" facts for "free". (Well, you'd have to prove them ...

4

Going off in a tangent here, program generators (i.e., systems that given a high-level description of something in some special language) have been around forever. Any compiler is one of those, as is any of the many parser generators. Back in the day systems called "third generation languages," which generated (most of the) code of a typical business ...

4

First of all, let's simplify f just a little bit, keeping the special case when it doesn't let the trailing /\ True to appear in the generated proposition (I also renamed the parameter names to make them correspond to the ones used by the theorem below): Fixpoint f' (i j : nat) : Prop := match j with | 0 => True | 1 => x i | S j' => f' i j' /\ ...

Only top voted, non community-wiki answers of a minimum length are eligible