Skip to main content
Stack Overflow
  1. About
  3. For Teams
Filter by
Sorted by
Tagged with
1 vote
1 answer
59 views

Section 5.1.3 "Using views in intro patterns" of the book "Mathematical Components" explain how the view intro-pattern works as follows. First, we have a lemma andP which relates (...
hengxin's user avatar
  • 2,011
0 votes
2 answers
124 views

I have an inductive type Inductive fin : nat -> Set := | First : forall n, fin (S n) | Next : forall n, fin n -> fin (S n). Coq cannot deduce that if something is of type fin 1 then it must be ...
Wiktor's user avatar
  • 301
1 vote
3 answers
87 views

When I prove with Coq (or Rocq), I find that sometimes if a hypothesis is "P" and another is "P -> forall x, Q x", I cannot make "forall x, Q x" a new premise by modus ...
0 votes
0 answers
40 views

I am working on proving the correctness of a Priority Queue implementation in Coq. I am getting stuck in the else branch of my insert theoreom. (I had to change my OG inductive hypothesis to better ...
1 vote
1 answer
67 views

Im trying to prove a correctness theorem for insert into a list-based priority queue. Here's the insert function, the inductive property, and the proof I'm working with: Fixpoint insert (x : nat) (l : ...
0 votes
0 answers
75 views

I'm quite new to Coq, I have done several projects in OCaml before and I'm doing this as a preparation for a course I'm taking next semester. A friend recommended the exercise of proofing the ...
0 votes
1 answer
113 views

I have to solve this exercise: Formulate and prove a confluence theorem for lambda calculus (ie, prove that if a λ-expression e reduces to both e1 and e2, then there exists e' such that e1 and e2 ...
0 votes
1 answer
98 views

I want to prove 2 step induction for list by using fix tactic In the following attempt to prove it I made goal structurally smaller(by applying pxy to the goal) before calling self, so I expect that ...
0 votes
2 answers
104 views

Consider following mutual inductive proposition Inductive TypeA : Prop := | ConstructorA : TypeB -> TypeA with TypeB : Prop := | ConstructorB : TypeA -> TypeB. Here is proof of ~TypeA in ...
nnarek's user avatar
  • 29
1 vote
2 answers
71 views

Here's what I'm trying to prove: Theorem add_n_injective : forall n m p, n + m = n + p -> m = p. I've tried Coq's built-in tactices, but they don't work. Is there an easy way to prove this? Here's ...
0 votes
1 answer
66 views

I have a puzzling situation in Coq where I'm working with relations and ensembles. I have defined coercions between them and a tactic to solve membership goals: Require Import Lia Reals Lra ...
0 votes
1 answer
106 views

I'm trying to formalize a stable-coin protocol using the Coq Interactive Theorem Prover. The proofs I have involve a lot of manipulation of linear and non-linear equations involving rational numbers. ...
1 vote
1 answer
73 views

I would like to create Coq tactics for solving a wide range of equality subgoals that may be solved by using a mix of rewrite rules such as associativity and commutativity of operators. Although this ...
cymbaz's user avatar
  • 45
0 votes
2 answers
151 views

I want to prove the inversion of inequality on negation, in natural numbers: forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j. I attempt to prove ...
Kaiwen's user avatar
  • 377
2 votes
0 answers
144 views

I need to prove A =~ Star re -> B =~ Star re -> A ++ B =~ Star re. in order to prove Pumping Lemma. These are the available match rules: Inductive exp_match {T} : list T -> reg_exp T -&...

15 30 50 per page
1
2 3 4 5
...
28

AltStyle によって変換されたページ (->オリジナル) /