Hot answers tagged

25

My preference is for Coq, but I imagine that others prefer Isabelle. One of the strange things I found about Isabelle is that there is a two-level syntax, where some of your definitions need to be inside double quote. No such nonsense is present in Coq. Ultimately, the one that is most suitable for you may depend on what you want to prove. Both languages ...


23

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). ...


18

One thing that I think you'll find interesting is that the "theorem proving" term varies vastly depending on what field you're in. While they are -- in the abstract -- somewhat related, practical theorem proving (like the kind you see elaborated on in the Handbook of Automated Reasoning) has less to do with Coq or Isabelle than you would think. When I ...


15

There is a variety of systems for Interactive Theorem Proving (ITP) -- see also the conference of that name -- Coq, Isabelle, HOLs, ACL2, PVS etc. All of them are relatively challenging to learn, and each has its own specific culture. It is like learning a foreign language: lets say you know English already, and then have the choice of French, German, ...


14

What works If you nest the definition of the fixpoint on lists inside the definition of the fixpoint on trees, the result is well-typed. This is a general principle when you have nested recursion in an inductive type, i.e. when the recursion goes through a constructor like list. Fixpoint size (t : LTree) : nat := let size_l := (fix size_l (l : list LTree)...


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 ...


13

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 ...


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. ...


10

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 ...


10

Here are some nice video Coq tutorials by Andrej Bauer. It's in no way complete, but I think it's a good introduction.


9

This has come up on the Coq mailing list several times, but I never saw a conclusive answer. Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity. Positivity enough is not enough, however, when you go outside Set; this example came up in several ...


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

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 ...


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

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 -&...


8

Ralph Matthes describes how to simulate types like this in Coq in "A Datastructure for Iterated Powers" (code, paper).


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

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 ...


7

The standard library of Coq has a section about real numbers. These are the classical real numbers, using the Dedekind completion. There are also results about complex numbers, I suppose there are several libraries, I happen to know this one. Note that there is also a lot of results for constructive real and complex numbers, C-CoRN is the reference. Side ...


7

This is obviously a problem specific to Coq since I believe there are nicer ways to get around it with some other proof assistants (I'm looking at Agda) At first I thought r was not recognized as structurally smaller because the structure is only about the inductive definition currently handled by Fixpoint: so this is not a LTree subterm even if it is a ...


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

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.


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 ...


6

One of the first things Coq does is building the induction principle associated with the inductive type you just defined and understanding the underlying induction principle is a good exercise. For example O : nat | S : nat -> nat will generate the induction principle P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n. What would be the induction ...


6

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 ...


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,...


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