coq Questions

2

Solved

I'm building a recursive function that does a match on a list l. In the cons branch I need to use the information that l = cons a l' in order to prove that the recursive function terminates. Howeve...
Seifert asked 5/12, 2014 at 12:48

3

I am working on the proof of the following theorem Sn_le_Sm__n_le_m in IndProp.v of Software Foundations (Vol 1: Logical Foundations). Theorem Sn_le_Sm__n_le_m : ∀n m, S n ≤ S m → n ≤ m. Proof. ...
Thill asked 24/5, 2019 at 12:12

3

Solved

During a proof, I encountered an hypothesis H. I have lemmas: H -> A and H -> B. How can I duplicate H in order to deduce two hypotheses A and B ? edited: More precisely, I have: lemma l1...
coq
Fissionable asked 7/12, 2014 at 15:34

0

I have a very long list of coq projects I want to automatically install with opam pin/install. I'd like to install them with opam because I am using this python tool (PyCoq) that uses opam pin/inst...
Electuary asked 20/8, 2022 at 13:23

2

I am currently using the standard one I installed the standard way (probably through the website). But I want to use tcoq. I believe I have installed it correctly because I have a bin file and all ...
Haletta asked 28/1, 2019 at 1:33

1

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 ...
coq
Douma asked 11/6, 2022 at 17:8

2

I got a new machine (mac book m1, not sure if it matters) and I noticed I didn't have Coq: (base) brandomiranda~ ❯ coqc -v zsh: command not found: coqc So I went to the instructions to download c...
coq
Summit asked 14/2, 2022 at 20:20

2

Solved

When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do. Lemma strange1: forall T:Type, 0&g...
Heavyarmed asked 5/12, 2014 at 19:8

1

Solved

I have imported a Coq module which defines a coercion, but it does not fit my needs. Is there any way to remove or (locally) override it? To be specific, say the module I imported defines a coerci...
Kimbell asked 22/12, 2018 at 5:31

4

Solved

Basically, I would like to prove that following result: Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) -> forall n, P n. that is the recurrence scheme...
Groan asked 5/10, 2013 at 16:41

2

Solved

In https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1 one can read: Coq's standard library takes a very different approach to the real numbers: An axiomatic approach. and one can find the following...
Miseno asked 22/10, 2021 at 22:39

1

Solved

I have the following two definitions that result in two different error messages. The first definition is declined because of strict positivity and the second one because of a universe inconsistenc...
Whopper asked 15/5, 2019 at 7:15

2

I find my self (sort of) duplicating code because I want to the same tactics in the goal and in a hypothesis when they match. For example: match goal with | H : PATTERN |- _ => simpl in H; rewri...
coq
Wampler asked 23/9, 2021 at 10:58

1

Solved

I've been working on a formalization for a process calculus in Coq (repository here), and constantly find myself trying to apply a function which fails because of equivalent, but syntactically diff...
Auriferous asked 17/9, 2021 at 20:20

1

Solved

I am trying to complete the series of exercises le_exercises from Logical Foundations' chapter on inductive propositions. This series is mostly based on the inductive relation le, defined thusly: I...
Edouard asked 5/9, 2021 at 14:27

4

Solved

[I am not sure this is appropriate for stack overflow, but there are many other Coq questions here so perhaps someone can help.] I am working through the following from http://www.cis.upenn.edu/~b...
Hepzi asked 1/11, 2011 at 12:9

2

Solved

Is it possible to switch the current goal or subgoal to prove in Coq? For example, I have a goal like this (from an eexists): ______________________________________(1/1) ?s > 0 /\ r1 * (r1 + s...
Anosmia asked 22/12, 2015 at 17:10

4

Solved

So this is one of the exercise I have been working from Software Foundations in which I have to prove that multipication is commutative. And this is my solution: Theorem brack_help : forall n m p:...
coq
Filings asked 13/1, 2016 at 4:39

1

Solved

Suppose I write the following lemma and proof in Coq: Lemma foo : forall A, A -> A. Proof. - simpl. - auto. Qed. The simpl here doesn't do anything, and this is a bad use of bullet points (-)...
coq
Catechism asked 16/7, 2021 at 12:14

1

I've been trying to understand what Set is after encountering it in Adam Chlipala's book in addition to this great discussion in SO. His first example definition binary ops using Set: Inductive bin...
coq
Beluga asked 20/6, 2021 at 14:45

3

I'm new to Coq, working on set-theoretic proof writing. I realized that parentheses are omitted, and it makes difficult for me to read the formula. For example, 1 subgoal A, B : {set T} H : B \su...
Hofmann asked 4/10, 2016 at 3:0

2

Solved

I know that one can extract Coq programs into Haskell and OCaml programs. Is there a way to do this with C? I am imagining a library that models the C language. Maybe such a library would contain...
Sulfapyridine asked 23/10, 2017 at 21:3

3

Solved

One finds that Setoids are widely used in languages such as Agda, Coq, ... Indeed languages such as Lean have argued that they could help avoid "Setoid Hell". What is the reason for using...
Grayback asked 29/12, 2020 at 14:24

1

Solved

Consider the situation described by the code below, wherein I have a "piecewise" function h behaving differently (like f, or like g) depending on some (decidable) property condition of it...
coq
Landwaiter asked 22/7, 2020 at 4:57

2

Solved

When proving in Coq, it's nice to be able to prove one little piece at a time, and have Coq help keep track of the obligations. Theorem ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B...
coq
Luthuli asked 12/3, 2020 at 21:29

© 2022 - 2024 — McMap. All rights reserved.