Questions tagged [coq]
Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.
2,952
questions
1
vote
1
answer
40
views
InteractionTrees library - simple program on ASM
I am trying to write simple program on ASM (a simple control-flow-graph language) from this tutorial:
InteractionTrees -> ASM.v
My final goal is to prove its correctness, using the library's ...
1
vote
1
answer
80
views
Installing Coq on Windows on GitHub Actions succeeds on a repo, and fails on another repo
I'm trying to install Coq on Windows on GitHub Actions, but seeing strange results.
I tried the following script, but couldn't install Coq because of the missing gmp.h error.
name: CI
on:
push:
...
- 874
0
votes
1
answer
45
views
How to instruct `auto` to simplify the goal during proof search?
A minimal example of my issue looks as follows:
Goal let x := True in x.
This is immediately solved by simpl. auto., but auto. does not work.
In my actual case, the search tree is a bit bigger than ...
- 6,859
0
votes
0
answers
54
views
Inductive from CoInductive?
It is possible to represent CoInductive using parts that are Inductive.
As a simple example,
CoInductive stream A :=
| SCons : A -> stream A -> stream A
.
Arguments SCons {A}.
CoInductive ...
- 419
0
votes
1
answer
61
views
Is is possible to rename a coq term?
Sorry, I'm not sure if the title is the adequate question.
I have been going through Logical Foundations. In the Lemma "double_plus" i solved it with this solution:
Lemma double_plus : ...
- 71
1
vote
1
answer
46
views
Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
I'm studying this great library for Representing Recursive and Impure Programs in Coq
I am having problems with mutual recursion (very first example in documentation gives me an error)
https://...
0
votes
2
answers
87
views
Is there a function that returns a list of values with specific type in OCaml?
In Haskell, using listify with Data can extract values of a specific type from a deeply nested structure without lots of getters. For example, with the following code:
{-# LANGUAGE DeriveDataTypeable #...
- 874
2
votes
1
answer
85
views
How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
I know how to prove 3 + 2 = 5 using Imp, defined in Software Foundations, Volume 1.
Definition plus2_3_is_5: Prop := forall (st: state),
(X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = ...
1
vote
1
answer
52
views
Showing polynomial equality in coq/ssreflect
I am trying to prove equality of polynomials by explicit computation in coq. Here's an example showing where I get stuck:
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit ...
- 201
-1
votes
1
answer
44
views
Syntax of the case tactic in coq
Can someone explain to me what the following coq tactic is doing?
case x : fun H => [|[]] // _.
How would I rewrite this using destruct?
Even better, can anyone point me to somewhere in the coq ...
- 201
0
votes
0
answers
69
views
Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
I was reading the paper Definitional proof-irrelevance without K, which states, in page 3, that
If proof irrelevance holds for the equality type, every equality has at most one proof, which is known ...
1
vote
1
answer
43
views
Understanding nat_ind2 in Logical Foundations
As an alternative induction principle of nat, nat_ind2 is defined like so:
Definition nat_ind2 :
forall (P : nat -> Prop),
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S(S n))) ->
...
- 205
0
votes
1
answer
58
views
What `dependent induction` tactic does in Coq and how to use it
Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough ...
- 463
0
votes
2
answers
63
views
Split multiple conjuncts in the goal
Is there a tactic to split multiple conjuncts in a goal into subgoals?
If I have the goal P /\ Q /\ R, I want to split it to produce three subgoals at once:
P, Q, and R
I can't seem to find any info ...
- 205
1
vote
1
answer
62
views
Coq can't define an inductive proposition
My Coq compiler is not allowing for inductive propositions as:
Inductive relation : nat -> nat -> Prop :=
| A : relation 1 2
| B : relation 2 3.
Throws: Error: The reference B was not found ...
- 305