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.

coq
Filter by
Sorted by
Tagged with
0 votes
1 answer
187 views

Cannot focus on a remaining unfocused goal in Coq

I am trying to prove the pumping Lemma (which is one of the exercises of the Logical Foundations book). I thought I had completed the MStarApp case but the interpreter tells me that there are still ...
user566206's user avatar
0 votes
2 answers
147 views

MAXIMUM VALUE OF THE LIST

I have list of natural numbers and its maximum value is not zero. I also have contra statement that value at index nth k l 0 is greater than maximum value.How I can prove that this wrong statement?...
niha kee's user avatar
1 vote
1 answer
56 views

Best way to make a relation associative in Coq

I’ve a relation C that takes three parameters. It represents an operation of my theory. So C(a, b, c) represents a = b @ c, however I didn’t (succeed to) define this operator in Coq, so I use only the ...
Lepticed's user avatar
  • 379
0 votes
0 answers
257 views

Stuck at the MApp case in Logical Foundation's pumping lemma

I am teaching myself to use the Coq proof assistant through the Logical Foundations course. I am stuck trying to prove the MApp case of the pumping lemma. Lemma pumping : forall T (re : reg_exp T) s, ...
user566206's user avatar
0 votes
1 answer
65 views

How can I write a nat in the form of term?

All I am trying to complete the last execrise in the StlcProp of Software Foundations Vol2. But I got stuck at defining step, in the rule ST_SuccNat. Inductive step : tm -> tm -> Prop := | ...
Jimmy Stone's user avatar
2 votes
1 answer
299 views

Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53)

I'm writing Agda code as I read the HoTT book. I'm stuck on Lemma 2.3.9: data _≡_ {X : Set} : X -> X -> Set where refl : {x : X} -> x ≡ x infix 4 _≡_ -- Lemma 2.1.2 _·_ : {A : Set} {x y z ...
Nuclear Catapult's user avatar
2 votes
2 answers
72 views

Evaluate constant inequation in Coq

I am trying to prove this : Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0. This is what I've done so far : Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -&...
op325's user avatar
  • 169
1 vote
2 answers
145 views

Coq - prove that there exists a maximal element in a non empty sequence

As an exercise I want to prove that there is always exists a maximum element in a non-empty sequence. Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -&...
dvr's user avatar
  • 370
1 vote
1 answer
66 views

Case analysis on max - ssreflect

I have the following in my goal: maxr x0 x I would like to do a case analysis, to consider what happens in the case that x0 is greatest, and the case the x is greatest. Is this possible in ssreflect? ...
dvr's user avatar
  • 370
2 votes
1 answer
70 views

How to improve this proof?

I work on mereology and I wanted to prove that a given theorem (Extensionality) follows from the four axioms I had. This is my code: Require Import Classical. Parameter Entity: Set. Parameter P : ...
Lepticed's user avatar
  • 379
0 votes
1 answer
65 views

Is this Lemma true in first-order intuitionistic logic?

I have the following first-order lemma: Lemma nop_firstorder : forall (n n1 n2:nat) (input: list nat), ( (exists p : prog, isValidProg p input -> execProg p [] input = Some [n;n1;n2])...
FH35's user avatar
  • 85
0 votes
1 answer
300 views

What is the best practice for installing external dependencies in a Coq project?

I understand what I believe is the essence of the official utilties doc https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project: one creates a _CoqProject with arguments to ...
Charlie Parker's user avatar
0 votes
1 answer
1k views

How does one import the lia tactic given that the omega tactic was reprecated in Coq?

I got the error: Error: The reference lia was not found in the current environment. how do I fix it? code: Require Import Lia. Theorem t: forall n: nat, 1 + n > n. Proof. Show Proof. ...
Charlie Parker's user avatar
2 votes
1 answer
444 views

redundant eval $(opam env) needed in Dockerfile [duplicate]

I successfully installed coqc with Dockerfile. Why do I need to run eval $(opam env) again when I execute the docker? ############## # # # image name # # # ############## FROM ...
OrenIshShalom's user avatar
3 votes
2 answers
142 views

Coq - Assign expression to variable

First and foremost, I'm not yet very familiar with Coq lingo, so I will use terms like e.g. 'expression' and 'variable' loosely, but they are probably not the correct Coq terms. I'm trying to prove ...
Mathieu Borderé's user avatar
0 votes
1 answer
292 views

Assume the negation of the goal in Coq

I'm trying to prove in Coq the following theorem: Theorem slot_company: forall s x, PPs s x -> exists t, PPs t x /\ s <> t. My current context and goal are: 1 subgoal s, x : Entity Pssx : ...
Lepticed's user avatar
  • 379
1 vote
1 answer
77 views

Can I prove a lemma without an additional inductive type

I have the following types : Inductive instr : Set := | Select : nat -> instr | Backspace : instr. Definition prog := list instr. and a function to 'execute' the program : Fixpoint execProg (...
FH35's user avatar
  • 85
0 votes
1 answer
63 views

Using the transitivity of equivalence to rewrite a goal

I want to prove the following theorem: Theorem T5: forall s t, (forall u, OoS s u <-> OoS t u) -> s = t. My current context and goal are: 1 subgoal s, t : Entity H : forall u : Entity, OoS ...
Lepticed's user avatar
  • 379
1 vote
1 answer
217 views

Unfolding terms created with `assert` in Coq

The proof in question can be found here. At the current state, I would like to unfold eqvid and eqvneg in hypothesis eqveq, in order to simplify the projection and obtain a contradictory equality ...
Michele De Pascalis's user avatar
0 votes
1 answer
63 views

Can't find a way to 'reverse' a constructor

I try to prove the following simple Lemma : Lemma wayBack : forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input. were implist is as follows : ...
FH35's user avatar
  • 85
1 vote
3 answers
870 views

User defined language in pandoc code-block

I'm trying to write a code-block in Coq (long story :)) inside pandoc. $ pandoc --list-highlight-languages | grep coq | wc -l 0 Since it doesn't exist, I wonder if there is an option to write my own ...
OrenIshShalom's user avatar
1 vote
1 answer
47 views

How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)?

I want to prove two characters are not equal. My environment currently looks like this: H: c1 = c2 -> not _____________________ Goal: (c1 =? c2)%char = false It won't allow me to apply H or ...
monique's user avatar
  • 11
0 votes
1 answer
46 views

is coq match statement exhaustive?

If i have a snippet similar to this one: Inductive Q : Set := | NULL : Q | CELL : nat -> Q -> Q -> Q . Definition someFunc (q: Q) := match q with | NULL => True | CELL 0 -> q1 -> ...
Nikolai Savulkin's user avatar
0 votes
1 answer
67 views

The reference info was not found in the current environment

I get The reference info was not found in the current environment when I try to do a make on the Adam Chlipala Certified Programming with Dependent Types download software cpdt bundle. The file is ...
147pm's user avatar
  • 2,187
0 votes
2 answers
32 views

How to evaluate square of a binom in coq?

I have reached a point in a structural induction proof where I have 2 equivalent algebraic expressions on different sides of the equation. One of them is just expanded form of another. I hoped ...
Nikolai Savulkin's user avatar
0 votes
1 answer
62 views

Add an assertion and its negation to Coq

I want to prove the following theorem: Theorem T1 : forall s x, Ps s x -> PPs s x /\ ~IPs s x \/ ~PPs s x /\ IPs s x. where Ps is a primitive and PPs and IPs are defined as follow (F is also a ...
Lepticed's user avatar
  • 379
1 vote
1 answer
367 views

Coq make failing on Omega

I'm trying to follow this but the provided source files are failing make with this error make[1]: Entering directory '/home/myhome/Dropbox/org/coq/cpdt' COQC src/CpdtTactics.v File "./src/...
147pm's user avatar
  • 2,187
1 vote
2 answers
98 views

Fail to prove a permutation property

I have created this simple type : Inductive implist : nat -> list nat -> Prop := | GSSingle : forall (n:nat), implist n [n] | GSPairLeft : forall (a b n:nat) (l:list nat), implist n l ->...
FH35's user avatar
  • 85
0 votes
1 answer
48 views

Is it possible to check the length of two strings before pattern matching against them?

I'm programming in Coq and want to eliminate non-exhaustive case matching by checking the length of the two strings first, for example Definition foo (word1 word2 : word) : option := if length ...
monique's user avatar
  • 11
1 vote
1 answer
211 views

Equivalence but not congruence

All I'm working on sf/plf chapter Equiv. There is an exercise We've shown that the [cequiv] relation is both an equivalence and a congruence on commands. Can you think of a relation on commands that ...
Jimmy Stone's user avatar
0 votes
2 answers
60 views

Cannot apply one hypothesis to another

I am very new to Coq and I'm trying to prove that if two functions are injectives, the composition of theses two functions is also injective. Here is my code: Definition compose {A B C} (g: B -> C) ...
Romain C's user avatar
0 votes
1 answer
65 views

Prove recursive function exists using only `nat_ind`

I'm trying to prove the following in Coq: ∀ B: Type, ∀ a: B, ∀ b: nat -> B -> B, ∃ f: nat -> B, f 0 = a ∧ ∀ n: nat, f (S n) = b n (f n). Which implies that a fairly general class of ...
hamid k's user avatar
  • 481
0 votes
1 answer
72 views

Fail to rewrite list with app_removelast_last

I have an environment which looks like this: P: list nat -> Prop Hnil: P [] ... xs, xp: list nat Hex: xp = a :: xs Hnilcons: xp <> [] =================== P xp I'd like to rewrite the goal to ...
FH35's user avatar
  • 85
0 votes
1 answer
186 views

How can i proof by absurd with coq?

I am reading Logical Foundations from Software Foundations series and i saw the plus_id_example that is: Theorem plus_id_example : forall n m:nat, n = m -> n + n = m + m. Proof. intros n m. ...
udduu's user avatar
  • 71
1 vote
2 answers
88 views

Proof on inductive type in Coq

I try to prove the following theorem: Theorem implistImpliesOdd : forall (n:nat) (l:list nat), implist n l -> Nat.Odd(length l). where implist is as follows : Inductive implist : nat -> list ...
FH35's user avatar
  • 85
1 vote
3 answers
198 views

Proof objects in the identity type

I'm reading through software foundation and they define equality as Inductive eq {X:Type} : X -> X -> Prop := | eq_refl : forall x, eq x x. Notation "x == y" := (eq x y) ...
Fernando Chu's user avatar
0 votes
1 answer
91 views

Precise control of conversion in Coq

I try to prove the following theorem in Coq: Theorem simple : forall (n b:nat) (input output: list nat) , short (n::b::input) true (n::output) = None -> short (b::input) false ...
FH35's user avatar
  • 85
1 vote
1 answer
63 views

Why coq doesn't use subtyping for logical or?

By subtyping, here I mean implicit coercion between types, not sig. In programming languages, sum types have associated data and it matters which variant is being used, so e.g. A can not be a subtype ...
hamid k's user avatar
  • 481
1 vote
2 answers
431 views

Why can I not apply f_equal to a hypothesis?

In my list of hypothesis, I have: X : Type l' : list X n' : nat H : S (length l') = S n' My goal is length l' = n'. So I tried f_equal in H. But I get the following error: Syntax error: [tactic:...
azani's user avatar
  • 486
1 vote
1 answer
92 views

How can I "specialize" a polymorphic type in Coq?

(Note, my goal is to learn more about Coq, not necessarily solve this particular problem. IRL, I expect I would just refactor to remove the offending type in that situation.) I have a type defined ...
azani's user avatar
  • 486
0 votes
2 answers
295 views

How to deal with division in COQ?

How to deal with with the division in a goal? Because I have a goal which is clearly true... However I cannot use lia and I think that this is related to the division. 2 ^ k / 2 ≤ 2 ^ k Bellow is my ...
Breno's user avatar
  • 155
0 votes
1 answer
83 views

Searching for a counterexample to a decidable predicate

It feels like the following Coq statement should be true constructively: Require Import Decidable. Lemma dec_search_nat_counterexample (P : nat -> Prop) (decH : forall i, decidable (P i)) : (~ (...
Rupert Swarbrick's user avatar
2 votes
1 answer
396 views

Adding an old version of Ocaml to Opam

I am trying to install Coq version 8.10.2 using Opam and from this output, I assume Coq 8.10.2 needs an ocaml compiler with version < 4.10 Missing dependency: - (invariant) -> coq = 8.10.2 -&...
Shubham Sondhi's user avatar
1 vote
1 answer
47 views

Symbolic manipulation of terms in Coq

Proof states like this often arise in my Coq studies: 1 goal n : nat IHn : fib_v1 n <= fib_v1 (S n) ______________________________________(1/1) fib_v1 (S n) <= fib_v1 (S (S n)) Coq complains ...
Attila Karoly's user avatar
0 votes
2 answers
131 views

In Coq, is there a way to prove a premise of a hypothesis conveniently?

I have H : P -> Q in my proof context, and I need Q to complete my proof, but I don't have any evidence of P: Is there a tactic or anything else that can make the premise P a new goal, then replace ...
Hoshino Tented's user avatar
0 votes
2 answers
158 views

How proof functions are combined in Coq

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 ...
Attila Karoly's user avatar
0 votes
0 answers
58 views

How can i model something with persistent state in coq?

In our university assignment we were asked to model the object of our choice in predicate and propositional logic. My group went for the 555 timer integrated circuit. We currently face the issue of ...
Nikolai Savulkin's user avatar
0 votes
1 answer
113 views

in coq how to assume equality of two natural numbers

I want to use this definition to assume that certain equalities on the members of set R hold: Definition wiring: Prop (globalHasVoltage -> (voltageOf voltageIn) = vcc) /\ (...
Nikolai Savulkin's user avatar
0 votes
1 answer
154 views

How to exhaust the match with in coq using something like default or or clause?

How can i write a switch state similar to this one (in rust), in coq? In particular I'm curios how to merge branches in coq to produce same output, and exhaust the remaining branches via some default ...
Nikolai Savulkin's user avatar
2 votes
2 answers
1k views

Proof by contradiction in Coq

I am trying to understand the apparent paradox of the logical framework of theorem provers like Coq not including LEM yet also being able to construct proofs by contradiction. Specifically the ...
Alan Audia's user avatar

1
3 4
5
6 7
59