**Feryll** posted a new question on June 24, 2020 at 10:39PM: **A suitably polymorphic definition of commutation in Coq – stackoverflow.com**

**Feryll** posted a new question on June 24, 2020 at 11:34PM: **Instantiating a class with a sig'd type in Coq – cs.stackexchange.com**

**rosi javi** posted a new question on June 25, 2020 at 02:20PM: **How to simplify lemma – stackoverflow.com**

**Max Heiber** posted a new question on June 26, 2020 at 04:39PM: **Does Gallina have an equivalent of Haskell's $ or Ocaml's @@ – stackoverflow.com**

**Carl Patenaude Poulin** posted a new question on June 26, 2020 at 07:40PM: **Simple syntax for terms of decidable subset types – stackoverflow.com**

**Carl Patenaude Poulin** posted a new question on June 26, 2020 at 07:43PM: **Under what circumstances is equality of equalities decidable? – stackoverflow.com**

**Max Heiber** posted a new question on June 27, 2020 at 11:22PM: **How can I rename an existentially quantified variable in a hypothesis? – stackoverflow.com**

**Sven Williamson** posted a new question on June 28, 2020 at 12:30PM: **Weak Excluded Middle Implies Morgan law for conjunction – stackoverflow.com**

**Frank Bryce** posted a new question on June 28, 2020 at 04:19AM: **Has reinforcement learning been used to prove mathematical theorems? – ai.stackexchange.com**

**push33n** posted a new question on June 28, 2020 at 11:54PM: **no error with assert (goal) but error with cut (goal) – stackoverflow.com**

**Carl Patenaude Poulin** posted a new question on June 29, 2020 at 07:52PM: **Configure OPAM switch for installation of Coq packages – stackoverflow.com**

**Mohammad-Ali A'RÂBI** posted a new question on July 01, 2020 at 01:43AM: **Cyclic type definition in Coq – stackoverflow.com**

**Jan Tušil** posted a new question on July 01, 2020 at 11:50AM: **How to communicate to Coq that certain types are equal? – stackoverflow.com**

**sdpoll** posted a new question on July 02, 2020 at 12:54AM: **How to get the type of a subterm when you're building a match – stackoverflow.com**

**TomR** posted a new question on July 03, 2020 at 07:32AM: **How to model/formalize the change of the variable (change of world) in Isabelle/HOL? – stackoverflow.com**

**ZhangLiao** posted a new question on July 05, 2020 at 12:02PM: **Arguments in tactics – stackoverflow.com**

**rosi javi** posted a new question on July 05, 2020 at 07:26PM: **How to prove statement is wrong – stackoverflow.com**

**rosi javi** posted a new question on July 07, 2020 at 06:08PM: **How to find difference between two statements – stackoverflow.com**

**rosi javi** posted a new question on July 07, 2020 at 06:08PM: **How to provide proof that two values are different? – stackoverflow.com**

**Marius Melzer** posted a new question on July 09, 2020 at 04:57PM: **Apply a lemma to a conjunction branch without splitting in coq – stackoverflow.com**

**raugfer** posted a new question on July 09, 2020 at 10:32PM: **Issue on definition expansion from Coq module system – stackoverflow.com**

**rosi javi** posted a new question on July 12, 2020 at 07:31PM: **How to arrange elements in the list – stackoverflow.com**

**A Question Asker** posted a new question on July 13, 2020 at 01:29PM: **Figuring out proper loop invariant when appending to a linked list with verifiable C – stackoverflow.com**

**A Question Asker** posted a new question on July 13, 2020 at 06:46PM: **Is it true that field_compatible (tarray (tptr tcell) 0)=(tptr tcell)? Is this approach to the body_incr correct? – stackoverflow.com**

**kimitsu** posted a new question on July 14, 2020 at 04:18AM: **Can't compare strings using Coq standard library – stackoverflow.com**

**frafle** posted a new question on July 15, 2020 at 03:26AM: **How can I create tuples in Coq and use them as new dataTypes – stackoverflow.com**

**A Question Asker** posted a new question on July 15, 2020 at 12:13PM: **Some help proving coq function terminates – stackoverflow.com**

**A Question Asker** posted a new question on July 15, 2020 at 01:01PM: **Dependent pattern match asks for a wildcard instead of proper type – stackoverflow.com**

**user2183336** posted a new question on July 15, 2020 at 05:42PM: **exp function in Coq doesn't appear to terminate – stackoverflow.com**

**user2183336** posted a new question on July 15, 2020 at 07:09PM: **First proof over Reals in Coq – stackoverflow.com**

**user2183336** posted a new question on July 15, 2020 at 09:04PM: **coq field tactic fails to simplify, yeilds "m <> 0%R" – stackoverflow.com**

**frafle** posted a new question on July 15, 2020 at 10:49PM: **How to use finite sets represented as lists in attributes of a class in Coq? – stackoverflow.com**

**user2183336** posted a new question on July 16, 2020 at 05:01PM: **Solve for a variable in Coq – stackoverflow.com**

**user2183336** posted a new question on July 16, 2020 at 06:39PM: **Show theorem definition in Coq – stackoverflow.com**

**Potiron** posted a new question on July 19, 2020 at 11:43AM: **How to define exp for Church Numerals in coq? – stackoverflow.com**

**A Question Asker** posted a new question on July 21, 2020 at 05:04PM: **Some help dealing with inject/unject and vector types – stackoverflow.com**

**Feryll** posted a new question on July 22, 2020 at 06:57AM: **Abstraction/typing error resulting from case_eq and rewriting in Coq – stackoverflow.com**

**rosi javi** posted a new question on July 22, 2020 at 08:44AM: **How to solve contradiction in Coq – stackoverflow.com**

**A Question Asker** posted a new question on July 23, 2020 at 12:03PM: **Improving dependently typed reverse function – stackoverflow.com**

**NJay** posted a new question on July 23, 2020 at 08:56PM: **Agda equivalent of destruct <term> eqn:<identifier> – stackoverflow.com**

**sana sobia** posted a new question on July 25, 2020 at 07:07AM: **How to apply a specific command – stackoverflow.com**

**A Question Asker** posted a new question on July 27, 2020 at 10:33AM: **Is there a way to get eauto to properly invoke econstructor? – stackoverflow.com**

**joshan beha** posted a new question on July 28, 2020 at 07:29PM: **How simply a statement of lemma – stackoverflow.com**

**user4035** posted a new question on July 28, 2020 at 10:13PM: **How to apply a lemma to 2 hypothesis – stackoverflow.com**

**user4035** posted a new question on July 28, 2020 at 11:25PM: **Coq: help to formalize an informal proof – stackoverflow.com**

**KöniglichePM** posted a new question on July 29, 2020 at 02:23PM: **How to get the name of a named goal in the coq api – stackoverflow.com**

**larsr** posted a new question on July 30, 2020 at 01:58PM: **Using Notations in Records – stackoverflow.com**

**user4035** posted a new question on July 30, 2020 at 06:31PM: **IndProp: prove that Prop is not provable – stackoverflow.com**

**user8845853** posted a new question on July 31, 2020 at 11:34PM: **How to instantiate hypotheses with variables that are out of scope – stackoverflow.com**

**Laila Elbeheiry** posted a new question on August 01, 2020 at 12:29AM: **Applying hypothesis with unknown variables – cstheory.stackexchange.com**

**Max Heiber** posted a new question on August 01, 2020 at 10:55PM: **Does using the unfold tactic followed by fold in Coq do anything? – stackoverflow.com**

**user5876164** posted a new question on August 04, 2020 at 08:29AM: **How to get cardinal of ensembles explicitly – stackoverflow.com**

**joshan beha** posted a new question on August 05, 2020 at 06:43PM: **Greatest value in natural number list – stackoverflow.com**

**user4035** posted a new question on August 06, 2020 at 11:11PM: **Instance of Ord typeclass for option – stackoverflow.com**

**HTNW** posted a new question on August 07, 2020 at 03:41AM: **How to prove all proofs of le equal? – stackoverflow.com**

**Max Heiber** posted a new question on August 08, 2020 at 03:15PM: **Would giving up on 'ex falso' change anything w.r.t. dependently-typed programming in Coq? – stackoverflow.com**

**Daisuke** posted a new question on August 09, 2020 at 11:28AM: **I have trouble on defining Category whose arrows are parametrised functions with Coq – stackoverflow.com**

**Lemming** posted a new question on August 09, 2020 at 12:10PM: **ring tactic on Z fails to simplify in exponent – stackoverflow.com**

**Daisuke** posted a new question on August 09, 2020 at 11:28AM: **define Category in which arrows are parametrised functions with Coq – stackoverflow.com**

**wt.cc** posted a new question on August 09, 2020 at 02:35PM: **What's the exact rule of applying a theorem in Coq? – stackoverflow.com**

**Daisuke** posted a new question on August 09, 2020 at 11:28AM: **define Category in which arrows are parametrised functions using Coq – stackoverflow.com**

**Francesca Pratali** posted a new question on August 10, 2020 at 05:16PM: **Coq for HoTT: proving || P-> X || -> (P-> ||X||) – stackoverflow.com**

**Rodrigo** posted a new question on August 12, 2020 at 11:56AM: **Proving technology of Coq's kernel – stackoverflow.com**

**push33n** posted a new question on August 12, 2020 at 07:07PM: **can coq intros pattern split at the rightmost opportunity for conjunction? – stackoverflow.com**

**user4035** posted a new question on August 12, 2020 at 10:18PM: **Coq: unary to binary convertion – stackoverflow.com**

**Rodrigo** posted a new question on August 13, 2020 at 11:29AM: **Difference between the logic and the type system of a proof assistant? – cs.stackexchange.com**

**Pedro Abreu** posted a new question on August 14, 2020 at 04:19AM: **Avoid implicit arguments of Fixpoint from becoming explicit in proof mode – stackoverflow.com**

**Artem Kokorin** posted a new question on August 14, 2020 at 08:04PM: **What are the rules of Coq implicit types deduction in Inductive definitions? – stackoverflow.com**

**push33n** posted a new question on August 14, 2020 at 09:59PM: **string comparison in ssreflect – stackoverflow.com**

**joshan beha** posted a new question on August 15, 2020 at 06:21PM: **How to close false statement of lemma – stackoverflow.com**

**push33n** posted a new question on August 15, 2020 at 09:13PM: **cannot rename things with dependent induction? – stackoverflow.com**

**Abe** posted a new question on August 21, 2020 at 03:35PM: **Not explicitly specifying instances of a type in coq – stackoverflow.com**

**joshan beha** posted a new question on August 22, 2020 at 08:24PM: **How to make constraints simple – stackoverflow.com**

**joshan beha** posted a new question on August 23, 2020 at 07:23PM: **Inversion tactics in coq – stackoverflow.com**

**Rodrigo** posted a new question on August 24, 2020 at 12:19PM: **What are the differences in the encoding of logics in Isabelle and Coq? – stackoverflow.com**

**Rodrigo** posted a new question on August 24, 2020 at 12:19PM: **How are logics encoded in Coq? – stackoverflow.com**

**Kaind** posted a new question on August 26, 2020 at 04:52PM: **"at next level" in Coq? – stackoverflow.com**

**Kaind** posted a new question on August 27, 2020 at 08:01PM: **Proof mode definitions in Coq? – stackoverflow.com**

**Tilman Zuckmantel** posted a new question on August 28, 2020 at 04:18PM: **Lemma about Sortedness of concatenated lists – stackoverflow.com**

**Kaind** posted a new question on August 29, 2020 at 08:21PM: **Reorder display of hypothesis in Coq? – stackoverflow.com**

**Sven Williamson** posted a new question on August 31, 2020 at 02:00PM: **Issue around the 'elim restriction' – stackoverflow.com**

**Rodrigo** posted a new question on August 30, 2020 at 05:59PM: **Does lean enhance proof surveyability? – stackoverflow.com**

**Rodrigo** posted a new question on September 01, 2020 at 05:22PM: **Can HOL be simulated in the CiC? – cs.stackexchange.com**

**Kaind** posted a new question on September 02, 2020 at 04:53PM: **Records as Prop? – stackoverflow.com**

**Kaind** posted a new question on September 02, 2020 at 04:57PM: **Curry Howard correspondance in Coq – stackoverflow.com**

**Kaind** posted a new question on September 02, 2020 at 04:57PM: **Curry Howard correspondence in Coq – stackoverflow.com**

**Kiran Gopinathan** posted a new question on September 03, 2020 at 05:14PM: **Verifying programs with heterogeneous arrays in VST – stackoverflow.com**

**Labbekak** posted a new question on September 03, 2020 at 07:24PM: **Coq: induction principles for void, unit and bool from nat and fin – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 07, 2020 at 11:11AM: **trivial theorem about my inductive type on Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 08, 2020 at 07:43AM: **Differential calculus on Coq – stackoverflow.com**

**joshan beha** posted a new question on September 08, 2020 at 06:39PM: **How to write statement formally? – stackoverflow.com**

**user3712960** posted a new question on September 09, 2020 at 01:17AM: **Backward Induction principle – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 09, 2020 at 06:36AM: **Pattern match with two list whose type is dependent type on Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 09, 2020 at 08:28AM: **exact value of the derivative on Coq – stackoverflow.com**

**Lance Pollard** posted a new question on September 10, 2020 at 07:47AM: **How do you lookup the definition or implementation of Coq proof tactics? – stackoverflow.com**

**joshan beha** posted a new question on September 10, 2020 at 09:22AM: **Equal relation between two terms – stackoverflow.com**

**Landon D. C. Elkind** posted a new question on September 14, 2020 at 03:02AM: **Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism) – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 15, 2020 at 11:46AM: **Partial derivative with Coquelicot on Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 15, 2020 at 02:39PM: **Partial differentiation using Coqelicot on Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 17, 2020 at 11:46AM: **Last n elements of list whose type is dependent type on Coq – stackoverflow.com**

**Daniel Hines** posted a new question on September 17, 2020 at 06:49PM: **Reusing lia tactic to prove decidability – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 18, 2020 at 02:35PM: **Vector error : The type of this term is a product – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 19, 2020 at 01:41PM: **Don't arrow arguments that don't meet conditions – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 20, 2020 at 04:35AM: **Can we ban arguments that don't meet conditions? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 21, 2020 at 01:24PM: **Guarantee the length of the list on Coq – stackoverflow.com**

**12412316** posted a new question on September 21, 2020 at 02:03PM: **Can I print the partial definition of not finished proof in coq? – stackoverflow.com**

**Rodrigo** posted a new question on September 21, 2020 at 07:51PM: **Using a module's definition in Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on September 21, 2020 at 01:24PM: **Transform the lemma leaving previous state on Coq – stackoverflow.com**

**Dole** posted a new question on September 24, 2020 at 04:04PM: **Defining Addition Over Integers in Coq – stackoverflow.com**

**Sajuuk** posted a new question on September 26, 2020 at 06:47AM: **Why isn't plus_assoc rewriting correctly? – cs.stackexchange.com**

**Sajuuk** posted a new question on September 26, 2020 at 07:33PM: **why is behaviour of simpl differ so much after a commutative operation and how to inspect simpl? – cs.stackexchange.com**

**Bob** posted a new question on September 26, 2020 at 08:35PM: **Impredicative Set and axioms – cstheory.stackexchange.com**

**Dan Johnson** posted a new question on September 29, 2020 at 10:18PM: **is there any tactic in Coq that can transform a bool expression to a Prop one? – stackoverflow.com**

**Joonazan** posted a new question on September 29, 2020 at 10:23PM: **How to index a tuple with ssreflect ordinals – stackoverflow.com**

**ewokonfire** posted a new question on September 30, 2020 at 01:16PM: **Coq: How do I prove that forall n m : nat, (n > m) -> (S n > S m)? – stackoverflow.com**

**Dan Johnson** posted a new question on October 02, 2020 at 04:13AM: **Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)" – stackoverflow.com**

**Dan Johnson** posted a new question on October 03, 2020 at 05:26PM: **Can I use destruct here given the constraint I have for index range of a list? – stackoverflow.com**

**Dan Johnson** posted a new question on October 05, 2020 at 04:13AM: **If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 05, 2020 at 03:21PM: **Append and Split is same as doing nothing – stackoverflow.com**

**Finn** posted a new question on October 05, 2020 at 06:24PM: **How can I prevent Coq notations in closed scopes interfering with notations in open ones? – stackoverflow.com**

**Morin** posted a new question on October 06, 2020 at 09:26AM: **Is there a tactic to help resolving existential qualifiers in Coq? – cs.stackexchange.com**

**Spielzeug** posted a new question on October 06, 2020 at 09:40AM: **Equality function in Coq – stackoverflow.com**

**Morin** posted a new question on October 06, 2020 at 09:26AM: **Is there a tactic to help resolving existential quantifiers in Coq? – cs.stackexchange.com**

**Daisuke Sugawara** posted a new question on October 06, 2020 at 02:17PM: **Vector : t A n = t A (n+0)? – stackoverflow.com**

**Dan Johnson** posted a new question on October 06, 2020 at 11:37PM: **Take a conjunction of two hypotheses and create a new hypothesis in Coq – stackoverflow.com**

**Dan Johnson** posted a new question on October 07, 2020 at 05:34AM: **How can I build a list of bytes from its specification in Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 07, 2020 at 09:51AM: **Vector: split a vector with n which is the same as vector's length – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 07, 2020 at 09:51AM: **Vector: theorem about splitting and appending vectors – stackoverflow.com**

**jvrn3** posted a new question on October 07, 2020 at 04:47PM: **What does Proof. simpl. reflexivity. Qed. mean in Coq? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 08, 2020 at 04:24PM: **Teach Coq that associative law of natural numbers holds – stackoverflow.com**

**nd2** posted a new question on October 09, 2020 at 02:46AM: **normalize (normalize n) = normalize (n) – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 09, 2020 at 02:51PM: **Vector: take out some elements from a vector with two methods – stackoverflow.com**

**user4035** posted a new question on October 10, 2020 at 09:26AM: **Quick Chick eqBoolArrowA_correct theorem – stackoverflow.com**

**user4035** posted a new question on October 10, 2020 at 10:40PM: **Coq Z_3 group definition left id theorem – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 11, 2020 at 10:41AM: **Prove equality of lists with list_beq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 11, 2020 at 01:43PM: **Equality on type which is not inductive type – stackoverflow.com**

**mia_h** posted a new question on October 11, 2020 at 04:03PM: **How to prove that the subsequence of an empty list is empty? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 12, 2020 at 07:59AM: **A list transformed from a vector equals to a list transformed from a vector casted its type – stackoverflow.com**

**Sajuuk** posted a new question on October 15, 2020 at 04:47AM: **Why discriminate the base case allows me to complete the induction proof? – cs.stackexchange.com**

**user4035** posted a new question on October 15, 2020 at 10:24AM: **Proof irrelevance for boolean equality – stackoverflow.com**

**user4035** posted a new question on October 15, 2020 at 04:54PM: **Z_3: left id proof – stackoverflow.com**

**TexasRattleSnake** posted a new question on October 16, 2020 at 08:25AM: **Inductive proposition for sublists in Coq – stackoverflow.com**

**mia_h** posted a new question on October 16, 2020 at 11:45PM: **How to apply a constructor in an hypothesis? – stackoverflow.com**

**user4035** posted a new question on October 17, 2020 at 12:35AM: **Z_3: left inversion lemma. How to add 1 + 1 + 1 – stackoverflow.com**

**gust** posted a new question on October 17, 2020 at 11:22PM: **Coq unable to unify -- how to change hypothesis? – stackoverflow.com**

**user4035** posted a new question on October 17, 2020 at 12:35AM: **Z_3: left inversion lemma – stackoverflow.com**

**Lessness Randomness** posted a new question on October 18, 2020 at 05:08PM: **How to prove equivalence between those two types - algorithm' and algorithm''? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 21, 2020 at 04:25PM: **Equality on complex functions – stackoverflow.com**

**Lessness Randomness** posted a new question on October 21, 2020 at 05:40PM: **Is there a good strategy for proving the given teorem? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 22, 2020 at 02:08PM: **Equality on complex functions part 2 – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 22, 2020 at 02:08PM: **Equality on complex functions with complex type – stackoverflow.com**

**sxysun** posted a new question on October 24, 2020 at 05:46AM: **Automatically proving a non-linear arithmetic proposition over Z in Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on October 26, 2020 at 12:03PM: **Different arguments, but behavior of function is same – stackoverflow.com**

**kimitsu** posted a new question on October 27, 2020 at 08:46AM: **Can't bind variable to wrapped open formula – stackoverflow.com**

**Lessness Randomness** posted a new question on October 21, 2020 at 05:40PM: **Is there a good strategy for proving the given theorem? – stackoverflow.com**

**Tejas Shah** posted a new question on October 28, 2020 at 05:59PM: **How does the grading script of the LF series work for manually graded exercises? – stackoverflow.com**

**Richard Southwell** posted a new question on November 03, 2020 at 06:30PM: **Dependent functions in Coq – stackoverflow.com**

**Richard Southwell** posted a new question on November 03, 2020 at 11:19PM: **Functions from empty set in Coq – stackoverflow.com**

**Baber** posted a new question on November 04, 2020 at 09:31AM: **Can we define recursive definitions in Coq? – stackoverflow.com**

**Yarick** posted a new question on November 05, 2020 at 12:31AM: **Stuck with a proof – stackoverflow.com**

**Leo Orshansky** posted a new question on November 07, 2020 at 08:44PM: **Coq - How can you apply an implication with a match clause? – stackoverflow.com**

**Taylor Roberts** posted a new question on November 08, 2020 at 08:13PM: **Predicate Logic in Coq – stackoverflow.com**

**MayJuneJuly** posted a new question on November 09, 2020 at 11:12AM: **Predicate Logic in coq: red tactic – stackoverflow.com**

**MayJuneJuly** posted a new question on November 09, 2020 at 11:12AM: **Predicate Logic in coq: – stackoverflow.com**

**user2809176** posted a new question on November 09, 2020 at 04:55PM: **Coq destruct with an excluding precondition – stackoverflow.com**

**MayJuneJuly** posted a new question on November 09, 2020 at 06:46PM: **Coq syntax. Predicate Logic – stackoverflow.com**

**blaineh** posted a new question on November 11, 2020 at 03:09AM: `match goal`

doesn't match let destructuring expression – stackoverflow.com

**Iaroslav Baranov** posted a new question on November 11, 2020 at 01:07PM: **Has somebody tried to use a proof assistant (coq) to do exercises from Cormen or Knuth? – stackoverflow.com**

**Miguel N.** posted a new question on November 11, 2020 at 03:29PM: **Error when defining custom notation for an embedded logic – stackoverflow.com**

**gust** posted a new question on November 12, 2020 at 05:05PM: **Make two arbitrary variables the same in Coq – stackoverflow.com**

**gust** posted a new question on November 12, 2020 at 10:13PM: **Stuck on Coq proof with list induction – stackoverflow.com**

**Max Heiber** posted a new question on November 14, 2020 at 04:21PM: **Coq: Syntax error 'Type' or 'Types' expected after 'Implicit' – stackoverflow.com**

**Mickelsinver** posted a new question on November 14, 2020 at 09:26PM: **Handling forall inside an hypothesis – stackoverflow.com**

**Youhei Okubo** posted a new question on November 15, 2020 at 07:27AM: **How can I construct terms in first-order logic using Coq? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 15, 2020 at 11:52AM: **Prove equation involving partial derivative analytically with Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 17, 2020 at 03:30AM: **diffefentiation of (1/2)*(x-y)^2 on x is x - y – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 17, 2020 at 08:43AM: **Difinition of equality among vectors – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 17, 2020 at 08:43AM: **Definition of equality among vectors – stackoverflow.com**

**Mickelsinver** posted a new question on November 19, 2020 at 12:58AM: **Can I avoid using Option A when I know that head cannot fail? – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 19, 2020 at 03:08PM: **Trivial lemma on real numbers on Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 20, 2020 at 12:33PM: **Theorem about vectors and recursive functions – stackoverflow.com**

**Jacob Keunen** posted a new question on November 20, 2020 at 01:49PM: **Induction with other base case in Coq – stackoverflow.com**

**manfey** posted a new question on November 21, 2020 at 02:22PM: **Translating coq statment to 'math' – mathoverflow.net**

**user2809176** posted a new question on November 22, 2020 at 04:02PM: **Coq prove a false list assumption – stackoverflow.com**

**Daisuke Sugawara** posted a new question on November 23, 2020 at 12:29PM: **split tail of the vector and append head of same vector – stackoverflow.com**

**Pierre Jouvelot** posted a new question on November 26, 2020 at 11:28AM: **Type coercion from nat to rat – stackoverflow.com**

**Nikita Mescheryackov** posted a new question on November 27, 2020 at 12:20AM: **Proofs of simple arithmetic expressions – stackoverflow.com**

**Jan Tušil** posted a new question on November 27, 2020 at 08:03PM: **Unable to satisfy the following constraints: In environment – stackoverflow.com**

**Alex Coleman** posted a new question on November 30, 2020 at 10:44PM: **Unable to find Coq library: Error: Unable to locate library Floats. – stackoverflow.com**

**Daisuke Sugawara** posted a new question on December 01, 2020 at 08:57AM: **Differentiate inner product on a element of a vector – stackoverflow.com**

**Tony Peterson** posted a new question on December 02, 2020 at 05:04PM: **Why are all numeric literals in Coq showing nat type? – stackoverflow.com**

**gust** posted a new question on December 03, 2020 at 07:07AM: `coqc -Q`

returns "coqc: -Q: no such file or directory" – stackoverflow.com

**Daisuke Sugawara** posted a new question on December 03, 2020 at 10:27AM: **Match the original value of the pattern match with branch value – stackoverflow.com**

**ZhangLiao** posted a new question on December 03, 2020 at 09:06PM: **How could we specify the times of running a tactic – stackoverflow.com**

**Daisuke Sugawara** posted a new question on December 04, 2020 at 06:32AM: **Differentiate the function id on an element of vector – stackoverflow.com**

**mia_h** posted a new question on December 04, 2020 at 02:49PM: **Arithmetic expressions and big-step semantic – stackoverflow.com**

**Mark** posted a new question on December 04, 2020 at 09:11PM: **Modeling Cardinality of Finite Sets in Coq – stackoverflow.com**

**R2D2** posted a new question on December 06, 2020 at 08:14AM: **How do I write a proof for a switch statement with VST/ coq? – stackoverflow.com**

**Sven Williamson** posted a new question on December 06, 2020 at 04:48PM: **Existence of a bijection between nat and nat * nat in Coq – stackoverflow.com**

**Daisuke Sugawara** posted a new question on December 07, 2020 at 12:34PM: **VecUtil: take nth element of processed vector by two slightly different way – stackoverflow.com**

**kimitsu** posted a new question on December 10, 2020 at 05:33PM: **How to prove forall x : R, 0 < x -> 0 < x / 2 < x? – stackoverflow.com**

**Max Heiber** posted a new question on December 11, 2020 at 11:51AM: **Is the only difference between Inductive and CoInductive the well-formedness checks on their uses (in Coq)? – stackoverflow.com**

**Max Heiber** posted a new question on December 11, 2020 at 12:19PM: **Is it possible to define a tactic that unfolds a cofix by one step in Coq? – stackoverflow.com**

**joshan beha** posted a new question on December 11, 2020 at 06:10PM: **less than relation between two natural numbers – stackoverflow.com**

**Blueper** posted a new question on December 13, 2020 at 02:25PM: **is there a tactic (other than inversion) that extracts implications from hypotheses? – stackoverflow.com**

**Warrick Macmillan** posted a new question on December 15, 2020 at 09:44PM: **Record Subtyping in Coq, questions and references requested – stackoverflow.com**

**geeky90846** posted a new question on December 17, 2020 at 05:10PM: **Simulation of global and local variables in Coq – stackoverflow.com**

**blaineh** posted a new question on December 19, 2020 at 04:48AM: **Induction order for relation between three lists – stackoverflow.com**

**Gregory** posted a new question on December 19, 2020 at 05:17AM: **Fine-grained builds with dynamic dependencies? – stackoverflow.com**

**Alex Coleman** posted a new question on December 21, 2020 at 02:56PM: **While it is expected to have type "forall..." in Coq – stackoverflow.com**

**joshan beha** posted a new question on December 21, 2020 at 05:23PM: **reduction in the elements of list – stackoverflow.com**

**Matheus Monteiro** posted a new question on December 21, 2020 at 10:07PM: **Defining functions inside proof scope – stackoverflow.com**

**joshan beha** posted a new question on December 22, 2020 at 06:46PM: **Counting of natural number – stackoverflow.com**

**Baber** posted a new question on December 23, 2020 at 06:05AM: **Why Coq doesn't allow a theorem with admits to end with QED in Linux and Windows? – stackoverflow.com**

**zeesha huq** posted a new question on December 23, 2020 at 06:30PM: **Effect of non zero term – stackoverflow.com**

**Hugo Carvalho de Paula** posted a new question on December 24, 2020 at 07:45PM: **What is the name of the programming style enabled by dependent types (think Coq or Agda)? – stackoverflow.com**

**joshan beha** posted a new question on December 25, 2020 at 07:42AM: **Conversion of a statement in formal language – stackoverflow.com**

**zeesha huq** posted a new question on December 28, 2020 at 08:53AM: **Less than relationship of natural numbers – stackoverflow.com**

**Henry Story** posted a new question on December 29, 2020 at 03:24PM: **Why do Calculus of Construction based languages use Setoids so much? – stackoverflow.com**

**John Smith** posted a new question on December 29, 2020 at 06:10PM: **How to pattern match exist to transform proofs – stackoverflow.com**

**blaineh** posted a new question on December 30, 2020 at 04:14AM: **How to debug tactic failure in a match goal branch? – stackoverflow.com**

**Hexirp** posted a new question on December 30, 2020 at 02:22PM: **How to print 'forall' as 'Π' in a one-time setting in coqdoc? – stackoverflow.com**

**joshan beha** posted a new question on December 30, 2020 at 05:35PM: **Finding a function from Library – stackoverflow.com**

**Isaac van Bakel** posted a new question on January 06, 2021 at 01:03AM: **How can I generalise Coq proofs of an iff? – stackoverflow.com**

**Hexirp** posted a new question on January 06, 2021 at 02:14PM: **Are we sure the Calculus of Inductive Constructions and ZFC plus countably many inaccessible cardinals are equiconsistent? – mathoverflow.net**

**joshan beha** posted a new question on January 06, 2021 at 04:54PM: **How to simplify counting relation between natural numbers – stackoverflow.com**

**Mahnoor dil** posted a new question on January 07, 2021 at 06:52PM: **prove a lemma sum of all elements of a list l is equal to n, (sortascend n) is equal to n – stackoverflow.com**

**joshan beha** posted a new question on January 08, 2021 at 05:51PM: **How to compare two elements of list – stackoverflow.com**

**Radu Deleanu** posted a new question on January 09, 2021 at 01:42AM: **Programming c-like classes to run in Coq – stackoverflow.com**

**Radu Deleanu** posted a new question on January 11, 2021 at 12:42AM: **list constructors conflict in Coq – stackoverflow.com**

**Wen Hui Fan** posted a new question on January 14, 2021 at 05:23AM: **Coq projects cannot be saved properly. Empty file – stackoverflow.com**

**Schluesselwolf** posted a new question on January 14, 2021 at 04:22PM: **Coq Newbie: How to iterate trough binary-tree in Coq – stackoverflow.com**

**juniorxx** posted a new question on January 16, 2021 at 07:46AM: **How to specialize nested hypotheses in Coq? – stackoverflow.com**

**Pierre Jouvelot** posted a new question on January 16, 2021 at 10:29PM: **Problems installing mathcomp 8.12/8.13 via nix on Catalina – stackoverflow.com**

**juniorxx** posted a new question on January 17, 2021 at 04:54PM: **How to formalize forall and exists in PLT Redex? – stackoverflow.com**

**user3565552** posted a new question on January 19, 2021 at 05:49AM: **What are the differences between LCF's Theorem and Automath's Prop? – cs.stackexchange.com**

**user3565552** posted a new question on January 20, 2021 at 03:06AM: **How do program types such as natural numbers figure into the Curry-Howard Isomorphism? – cs.stackexchange.com**

**push33n** posted a new question on January 20, 2021 at 03:59AM: **can i stack implicit types somehow? – stackoverflow.com**

**Not me** posted a new question on January 20, 2021 at 05:45AM: **How is an infinite type hierarchy implemented? – stackoverflow.com**

**ged** posted a new question on January 22, 2021 at 11:57AM: **Theorem that finding in a list works properly – stackoverflow.com**

**tts** posted a new question on January 23, 2021 at 08:41AM: **What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$? – cstheory.stackexchange.com**

**Charlie Parker** posted a new question on January 24, 2021 at 09:24PM: **How does one display the an arbitrary programming language (e.g. Isabelles Isar) in latex in their naive display in pdf? – stackoverflow.com**

**Charlie Parker** posted a new question on January 24, 2021 at 09:24PM: **How does one display an arbitrary programming language (e.g. Isabelle/Isar) in latex in their native display in *.pdf format? – stackoverflow.com**

**user4035** posted a new question on January 26, 2021 at 08:47PM: **Error when referencing type variable from another file – stackoverflow.com**

**Luiz Martins** posted a new question on January 28, 2021 at 06:17AM: **Printing ssrnat's ".+1" definition – stackoverflow.com**

**Izzy** posted a new question on January 28, 2021 at 09:43PM: **What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations? – stackoverflow.com**

**NJay** posted a new question on January 29, 2021 at 06:43PM: **Why can I use the constructor tactic to prove reflexivity? – stackoverflow.com**

**Luiz Martins** posted a new question on January 31, 2021 at 01:10AM: **Using the same variable multiple times in a definition to represent equality – stackoverflow.com**

**Walter Schulze** posted a new question on January 31, 2021 at 05:29PM: **Rewriting between two equivalent setoids – stackoverflow.com**

**Hexirp** posted a new question on February 02, 2021 at 08:12AM: **I know of two ways to define the finite number type. Is there words to distinguish between the two? – stackoverflow.com**

**Luiz Martins** posted a new question on February 02, 2021 at 10:10AM: **Introducing a new assumption/hypothesis by adding it as subgoal – stackoverflow.com**

**Walter Schulze** posted a new question on January 31, 2021 at 05:29PM: **Coq: Rewriting between two equivalent setoids – stackoverflow.com**

**Pierre Jouvelot** posted a new question on February 03, 2021 at 09:47PM: **Lost ".+1" Coq notation in Emacs Proof General Goals buffer – stackoverflow.com**

**Luiz Martins** posted a new question on February 04, 2021 at 10:05AM: **Difference between propositionals True/False and booleans true/false in Coq – stackoverflow.com**

**Quinn Dougherty** posted a new question on February 04, 2021 at 10:57AM: **Why is preservation not quantified over Gamma? – cstheory.stackexchange.com**

**fakedrake** posted a new question on February 05, 2021 at 03:03PM: **Proofs of structural properties of arguments in match in coq – stackoverflow.com**

**William Oliver** posted a new question on February 05, 2021 at 09:33PM: **Is it possible to prove forall n: nat, le n 0 -> n = 0. in Coq without using inversion? – stackoverflow.com**

**user15163266** posted a new question on February 07, 2021 at 05:28PM: **how to proof (f1+f1 = f2+f2 -> f1 = f2) in coq – stackoverflow.com**

**Khan** posted a new question on February 11, 2021 at 08:36AM: **Reasoning over functions applied to lists of nat in Coq – stackoverflow.com**

**user7508402** posted a new question on February 11, 2021 at 04:59PM: **Coq: parametric rewriting under binders – stackoverflow.com**

**William Oliver** posted a new question on February 12, 2021 at 10:16PM: **Removing trivial match clause in Coq – stackoverflow.com**

**joshan beha** posted a new question on February 14, 2021 at 11:19AM: **Lemma related to the counting of numbers in list – stackoverflow.com**

**Jordan Mitchell Barrett** posted a new question on February 16, 2021 at 10:56AM: **Defining integers inductively in Coq (inductive definitions subject to relations) – stackoverflow.com**

**Molossus Spondee** posted a new question on February 16, 2021 at 08:54PM: **Call by name untyped lambda calculus interpreter in Coq – codereview.stackexchange.com**

**Zhang Liao** posted a new question on February 17, 2021 at 03:18PM: **Puzzle of induction in Coq – stackoverflow.com**

**junius** posted a new question on February 18, 2021 at 03:28PM: **Compiling multiple Coq files does not work – stackoverflow.com**

**user5876164** posted a new question on February 20, 2021 at 03:34PM: **How to prove for all functions P, Q from typical type to Prop, "forall a, b, P(a) or Q(b) holds" iff "forall a, P(a), or, forall b, Q(b), holds"? – stackoverflow.com**

**Pierre Jouvelot** posted a new question on February 20, 2021 at 10:49PM: **Translating proof from Nat to Rat – stackoverflow.com**

**17L251.Swathi.S** posted a new question on February 23, 2021 at 08:17AM: **How to implement a spec and prove it using kami? – stackoverflow.com**

**Lance Pollard** posted a new question on February 27, 2021 at 06:47PM: **How to constrain a type field to a power of two in a type system? – stackoverflow.com**

**Lance Pollard** posted a new question on February 27, 2021 at 11:52PM: **How to does "there exists" existential quantifier work in an imperative language? – stackoverflow.com**

**radrow** posted a new question on February 28, 2021 at 01:57PM: **Proving coinductive theorems with coinductive assumptions – stackoverflow.com**

**NJay** posted a new question on March 01, 2021 at 10:52PM: **Theorem + induction vs Fixpoint + destruct in Coq – stackoverflow.com**

**Wen Hui Fan** posted a new question on March 03, 2021 at 09:47PM: **Use coq to define a special Nat Type as below – stackoverflow.com**

**Wen Hui Fan** posted a new question on March 04, 2021 at 07:56AM: **Define list length in recursion in Coq Not sure if my function is wrong and got stuck – stackoverflow.com**

**NJay** posted a new question on March 04, 2021 at 03:37PM: **Impredicativity + large eliminations (with no excluded middle) in Coq – cstheory.stackexchange.com**

**domino** posted a new question on March 06, 2021 at 11:25PM: **Define a polymorphic type in coq – stackoverflow.com**

**domino** posted a new question on March 07, 2021 at 02:39AM: **Define polymorphic inductive type tree in coq – stackoverflow.com**

**domino** posted a new question on March 07, 2021 at 08:23PM: **Anyone know how mult works in coq? – stackoverflow.com**

**rexor** posted a new question on March 11, 2021 at 12:51AM: **Recursive definition of nat_to_bin is ill-formed – stackoverflow.com**

**zeesha huq** posted a new question on March 13, 2021 at 05:34AM: **How to write gcd function in Coq – stackoverflow.com**

**Alex** posted a new question on March 15, 2021 at 12:15AM: **How to implement a union-find (disjoint set) data structure in Coq? – stackoverflow.com**

**shooqie** posted a new question on March 15, 2021 at 11:40AM: **Proving extentional equality of two functions – stackoverflow.com**

**Reed** posted a new question on March 15, 2021 at 09:01PM: **I need to derive a .v filetype from a .ott file – stackoverflow.com**

**Jordan Mitchell Barrett** posted a new question on March 16, 2021 at 06:44AM: **Coq: evaluating/simplifying Prop tautologies – stackoverflow.com**

**user1953221** posted a new question on March 16, 2021 at 10:19AM: **Case splitting on if-then-else condition – stackoverflow.com**

**Andrey** posted a new question on March 16, 2021 at 09:56PM: **Prove commutativity for the sum of two even numbers with dependent types – stackoverflow.com**

**einzwein** posted a new question on March 17, 2021 at 06:07AM: **Defining inductive types in intensional type theory purely in terms of type-theoretic data – cstheory.stackexchange.com**

**Andrey** posted a new question on March 16, 2021 at 09:56PM: **Postulate and prove theorem about equality for different types (Prove commutativity for the sum of two even numbers with dependent types) – stackoverflow.com**

**addtip** posted a new question on March 19, 2021 at 02:57PM: **Coq leb <=? does not give me an hypothesis after case or induction – stackoverflow.com**

**GhaS Shee** posted a new question on March 19, 2021 at 05:33PM: **coq-HoTT: How to prove 1 < 2? – stackoverflow.com**

**addtip** posted a new question on March 19, 2021 at 09:26PM: **Finding rewrite rules – stackoverflow.com**

**zeesha huq** posted a new question on March 20, 2021 at 05:37PM: **How to solve greater or equal relation between two numbers – stackoverflow.com**

**SD01** posted a new question on March 22, 2021 at 04:38PM: **Coq begginer here, how to understand the syntax? – stackoverflow.com**

**granduser** posted a new question on March 22, 2021 at 10:18PM: **Coq proving nonsensical inductive property implication? – stackoverflow.com**

**Andrew W** posted a new question on March 26, 2021 at 08:15AM: **In Coq, is there a way to see the tactics applied by tauto? – stackoverflow.com**

**zeesha huq** posted a new question on March 26, 2021 at 02:31PM: **Use of contradiction statement – stackoverflow.com**

**Jordan Mitchell Barrett** posted a new question on March 27, 2021 at 01:40AM: **Coq - function choosing witnesses for a forall-exists statement – stackoverflow.com**

**Jordan Mitchell Barrett** posted a new question on March 28, 2021 at 07:00AM: **Coq - adding choice function to context – stackoverflow.com**

**einzwein** posted a new question on March 28, 2021 at 12:26PM: **Dependent eliminator for empty type in intensional Martin-Löf type theory – cstheory.stackexchange.com**

**Shubham Sondhi** posted a new question on March 28, 2021 at 03:44PM: **How to deal with "false = true" proposition while proving theorems in coq – stackoverflow.com**

**LeBaguette** posted a new question on March 29, 2021 at 12:22AM: **How do I prove false from a false hypothesis? – stackoverflow.com**

**R. Bosman** posted a new question on March 29, 2021 at 06:13PM: **How do I exclude a certain form in a hint for autorewrite? – stackoverflow.com**

**D. Ben Knoble** posted a new question on March 30, 2021 at 02:14AM: **Unfold a type-function in a match (like destruct) – stackoverflow.com**

**R. Bosman** posted a new question on March 29, 2021 at 06:13PM: **Add ltac expression as hint to autorewrite? – stackoverflow.com**

**user65526** posted a new question on March 30, 2021 at 10:52AM: **Pairs and projections in Coq – stackoverflow.com**

**Jordan Mitchell Barrett** posted a new question on March 31, 2021 at 05:31AM: **Coq can't infer type parameter in match – stackoverflow.com**

**Philémon Berstel-Da Silva** posted a new question on March 31, 2021 at 10:38AM: **How to prove the decomposition of implication? – stackoverflow.com**

**domino** posted a new question on April 01, 2021 at 04:45AM: **define edges for undirected graph in coq – stackoverflow.com**

**Shubham Sondhi** posted a new question on April 02, 2021 at 01:13AM: **Coq proof stuck in a loop – stackoverflow.com**

**Shubham Sondhi** posted a new question on April 02, 2021 at 10:14AM: **Loop while proving a theorem – stackoverflow.com**

**Marco Servetto** posted a new question on April 03, 2021 at 12:21AM: **Coq Notation Syntax error: [term level 200] expected after [term level 200] (in [term]) – stackoverflow.com**

**steve01** posted a new question on April 03, 2021 at 03:22PM: **What tactic should I use to avoid stucking in endless loop, in Coq? – stackoverflow.com**

**rausted** posted a new question on April 05, 2021 at 12:46AM: **Coq Vector explode in proof mode? – stackoverflow.com**

**ieja** posted a new question on April 06, 2021 at 12:58PM: **Mix-up of bool and Datatypes.bool after Require Import coq libraries – stackoverflow.com**

**ieja** posted a new question on April 07, 2021 at 11:48AM: **Coq infotheo %B is_true – stackoverflow.com**

**domino** posted a new question on April 08, 2021 at 05:27AM: **How to prove one nat is less than or equal to another nat in coq? – stackoverflow.com**

**domino** posted a new question on April 08, 2021 at 09:28AM: **How to prove n <= n + S m in coq? – stackoverflow.com**

**D. Ben Knoble** posted a new question on April 08, 2021 at 06:24PM: **Dependent-type design when the parameters indicate the result should not exist – stackoverflow.com**

**Marco Mantovani** posted a new question on April 08, 2021 at 07:01PM: **FoldR using FoldL on finite lists – stackoverflow.com**

**Jan Tušil** posted a new question on April 08, 2021 at 07:55PM: **Tower of powersets – stackoverflow.com**

**ieja** posted a new question on April 09, 2021 at 09:26AM: **Coq infotheo Unable to Unify error when comparing sums of reals – stackoverflow.com**

**Veky** posted a new question on April 09, 2021 at 01:41PM: **coq auto says simple apply fails but it works manually – stackoverflow.com**

**ieja** posted a new question on April 10, 2021 at 12:01PM: **Cauchy-Schwartz Inequality in Coq? – stackoverflow.com**

**user15598472** posted a new question on April 10, 2021 at 02:31PM: **"Symbol's value as variable is void" when adding a path to coqtop when opening emacs – stackoverflow.com**

**domino** posted a new question on April 13, 2021 at 07:04AM: **Implement Boruvka's algorithm in Coq – stackoverflow.com**

**Kleiton Pereira** posted a new question on April 14, 2021 at 05:40PM: **coq - Unable to unify "None = Some x" with "Some (f x) = None" – stackoverflow.com**

**zeesha huq** posted a new question on April 15, 2021 at 04:48AM: **Use of build-In function in Coq – stackoverflow.com**

**domino** posted a new question on April 16, 2021 at 08:16PM: **Coq: Functions for finding the lightest weight edge. Error msg – stackoverflow.com**

**zeesha huq** posted a new question on April 17, 2021 at 01:56PM: **Counting of natural numbers in the list – stackoverflow.com**

**domino** posted a new question on April 18, 2021 at 09:29PM: **Is there anyway I can output all the shortest path in Coq? – stackoverflow.com**

**ieja** posted a new question on April 19, 2021 at 10:59AM: **MApp subgoal in Pumping lemma – stackoverflow.com**

**ieja** posted a new question on April 19, 2021 at 12:33PM: **Pumping lemma MStarApp case – stackoverflow.com**

**R. Bosman** posted a new question on April 20, 2021 at 12:25PM: **(genralized) rewriting of an equivalent term under constructor? – stackoverflow.com**

**ieja** posted a new question on April 20, 2021 at 12:25PM: **Coq proving addition inequality – stackoverflow.com**

**user7508402** posted a new question on April 20, 2021 at 03:56PM: **Coq: rewriting under if-then-else – stackoverflow.com**

**Houda** posted a new question on April 20, 2021 at 07:29PM: **Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot – stackoverflow.com**

**abeln** posted a new question on April 21, 2021 at 10:56PM: **Trigger typeclass search from auto/eauto – stackoverflow.com**

**Vaibhav G.** posted a new question on April 26, 2021 at 11:17PM: **How to represent kleisli composition of substitutions in abstract trees – stackoverflow.com**

**ieja** posted a new question on April 27, 2021 at 03:43PM: **Coq ssreflect sum of sums – stackoverflow.com**

**Fusen** posted a new question on April 27, 2021 at 08:39PM: **Compare sums ssreflect – stackoverflow.com**

**Kathy** posted a new question on April 28, 2021 at 12:18AM: **Rbar_le x 0 -> Rbar_le y 0 -> Rbar_le (Rbar_plus x y) 0 in Coq – stackoverflow.com**

**Fusen** posted a new question on April 28, 2021 at 12:52PM: **Ssreflect probabilities (event and not event) sum to one – stackoverflow.com**

**Karlo Kampić** posted a new question on April 29, 2021 at 10:27PM: **How to destruct a function (like H : ~ (forall x : X, p x)) in Coq? – stackoverflow.com**

**Kathy** posted a new question on April 28, 2021 at 12:18AM: **Rbar / Rbar_le / coquelicot lemma – stackoverflow.com**

**domino** posted a new question on April 30, 2021 at 10:45PM: **How to prove a odd number is the successor of double of nat in coq? – stackoverflow.com**

**domino** posted a new question on May 01, 2021 at 06:24AM: **Is it possible to prove oddb 0 = true?? coq – stackoverflow.com**

**DeeDee** posted a new question on May 01, 2021 at 02:58PM: **Using a theorem on integer numbers for proving a theorem on natural numbers – stackoverflow.com**

**VinaLx** posted a new question on May 03, 2021 at 12:18PM: **What does Control.refine do in Ltac2? – stackoverflow.com**

**joshan beha** posted a new question on May 04, 2021 at 07:26AM: **less or equal relation with largest element of natural number list – stackoverflow.com**

**David** posted a new question on May 12, 2021 at 12:42AM: **How to prove (~Q -> ~P) - > (P -> Q) in Coq – stackoverflow.com**

**Doyun Nam** posted a new question on May 14, 2021 at 10:29AM: **What does "eq^~" mean in Coq? – stackoverflow.com**

**Giacomo Maletto** posted a new question on May 16, 2021 at 06:37PM: **Can a function argument be scoped automatically in Coq? – stackoverflow.com**

**jayven** posted a new question on May 17, 2021 at 10:19AM: **Don't understand destruct tactic on hypothesis ~ (exists x : X, ~ P x) in Coq – stackoverflow.com**

**TalionZz** posted a new question on May 17, 2021 at 01:32PM: **Solving a mergesort split proof in Coq – stackoverflow.com**

**user1535186** posted a new question on May 21, 2021 at 12:11PM: **The type checker's behavior while pattern matching in Coq – stackoverflow.com**

**Mickey Mouse** posted a new question on May 22, 2021 at 08:27PM: **Definitions in Coq – stackoverflow.com**

**Cris Teller** posted a new question on May 23, 2021 at 01:25AM: **Strong specification in Coq – stackoverflow.com**

**user4035** posted a new question on May 23, 2021 at 08:50AM: **Is it possible to keep the original hypothesis while using intro pattern – stackoverflow.com**

**Cris Teller** posted a new question on May 23, 2021 at 05:20PM: **Inductive haskell's Replicate function in Coq – stackoverflow.com**

**Cris Teller** posted a new question on May 23, 2021 at 05:20PM: **Coq: Strong specification of haskell's Replicate function – stackoverflow.com**

**Cris Teller** posted a new question on May 24, 2021 at 02:35AM: **Coq - Proof of list pair – stackoverflow.com**

**push33n** posted a new question on May 24, 2021 at 04:16AM: **how to simplify basic arithmetic in more complex goals – stackoverflow.com**

**Cris Teller** posted a new question on May 24, 2021 at 03:03PM: **Coq: Prove Inductive relation (vs Fixpoint) – stackoverflow.com**

**Mickey Mouse** posted a new question on May 25, 2021 at 06:42PM: **Dealing with and sign in goal – stackoverflow.com**

**joshan beha** posted a new question on May 28, 2021 at 08:08PM: **How to find minimum element of natural number list – stackoverflow.com**

**Serene** posted a new question on May 30, 2021 at 07:52AM: **Coq: Recursive definition of fibonacci is ill-formed – stackoverflow.com**

**Kathy** posted a new question on June 04, 2021 at 06:02PM: **How to give the simple function its formula as a linear combination of indicator functions in Coq – stackoverflow.com**

**Eben Kadile** posted a new question on June 09, 2021 at 03:37PM: **Produce a function in Coq which outputs every witness to an existence-uniqueness axiom – stackoverflow.com**

**Saad** posted a new question on June 11, 2021 at 02:39PM: **True and False values of type Prop in Coq – stackoverflow.com**

**Yosuke Ito** posted a new question on June 12, 2021 at 02:16PM: **Is there any way to rewrite the function in "is_lim"? – stackoverflow.com**

**Cris Teller** posted a new question on June 13, 2021 at 06:24PM: **Coq: Cannot guess decreasing argument of fix – stackoverflow.com**

**Joshua Meyers** posted a new question on June 13, 2021 at 10:01PM: **Why does Record forget which arguments are implicit? – stackoverflow.com**

**Attila Karoly** posted a new question on June 15, 2021 at 12:52PM: **Is this a correct application of 'exists' in Coq? – stackoverflow.com**

**Tekkno** posted a new question on June 15, 2021 at 03:26PM: **How to generate Coq files from Frama-C WP plugin – stackoverflow.com**

**Felipe** posted a new question on June 17, 2021 at 08:13PM: **Composing sumbools for container type – stackoverflow.com**

**joshan beha** posted a new question on June 18, 2021 at 03:31AM: **How I can convert the relation between two terms in Coq – stackoverflow.com**

**Cris Teller** posted a new question on June 18, 2021 at 09:14PM: **Coq to Why3: with notation – stackoverflow.com**

**Andrey** posted a new question on June 19, 2021 at 09:27AM: **Why unable to perform case analysis in rather simple case – stackoverflow.com**

**August C.** posted a new question on June 20, 2021 at 02:55AM: **How do I translate static void and extern void from C to x86-64? – stackoverflow.com**

**Felipe** posted a new question on June 20, 2021 at 05:34AM: **How to write a 'safe' head in coq? – stackoverflow.com**

**Cris Teller** posted a new question on June 20, 2021 at 04:19PM: **Coq to Why3: Proof of aux lemma of function correction – stackoverflow.com**

**Charlie Parker** posted a new question on June 20, 2021 at 04:45PM: **What is a concrete example of the type Set and what is the meaning of Set? – stackoverflow.com**

**Cris Teller** posted a new question on June 18, 2021 at 11:28PM: **Why3: Proof with induction – stackoverflow.com**

**Mickey Mouse** posted a new question on June 20, 2021 at 09:07PM: **question about intros [=] and intros [= <- H] – stackoverflow.com**

**Giwon Song** posted a new question on June 21, 2021 at 01:41AM: **How to add "assumed true" statements in Coq – stackoverflow.com**

**Giwon Song** posted a new question on June 21, 2021 at 12:41PM: **How to use symmetricity of an equality on Coq – stackoverflow.com**

**Giwon Song** posted a new question on June 22, 2021 at 12:27AM: **How to prove simplification of logic(A and B implies A) in Coq – stackoverflow.com**

**Giwon Song** posted a new question on June 22, 2021 at 02:54AM: **proof of adding 1 to some number changes the parity in Coq – stackoverflow.com**

**pjm** posted a new question on June 22, 2021 at 06:21PM: **Implicit arguments propagation – stackoverflow.com**

**Attila Karoly** posted a new question on June 22, 2021 at 06:23PM: **Unifying types of identical meanings – stackoverflow.com**

**setholopolus** posted a new question on June 22, 2021 at 07:32PM: **Parametrizing a Module in Coq – stackoverflow.com**

**setholopolus** posted a new question on June 22, 2021 at 07:45PM: **Alternative tactic for ssreflect's move=> – stackoverflow.com**

**Felipe** posted a new question on June 23, 2021 at 03:56AM: **Proving two-list queue in coq – stackoverflow.com**

**Attila Karoly** posted a new question on June 23, 2021 at 11:13AM: **Computational behaviour of Successor – stackoverflow.com**

**Berelex** posted a new question on June 23, 2021 at 12:16PM: **Coq - trivial induction on lists doesn't accept assumtion – stackoverflow.com**

**Berelex** posted a new question on June 23, 2021 at 12:16PM: **(SOLVED - was a goal-printing bug) Coq - trivial induction on lists doesn't accept assumtion – stackoverflow.com**

**joshan beha** posted a new question on June 24, 2021 at 03:03AM: **How to apply/use buildin function – stackoverflow.com**

**98189per** posted a new question on June 24, 2021 at 08:35PM: **How do I prove an existential goal that asks for a certain function in Coq? – stackoverflow.com**

**Charlie Parker** posted a new question on June 24, 2021 at 08:57PM: **What does the at sign @ mean in Coq - especially in the context of Gallina terms? – stackoverflow.com**

**Charlie Parker** posted a new question on June 25, 2021 at 12:55AM: **How does one print the entire contents of a proof object or Gallina terms in Coq? – stackoverflow.com**

**push33n** posted a new question on June 25, 2021 at 06:19PM: **apply ltac to subexpression of a goal – stackoverflow.com**

**Bob** posted a new question on June 26, 2021 at 01:25PM: **Can I safely assume that isomorphic types are equal? – stackoverflow.com**

**KingsAlpaca** posted a new question on June 28, 2021 at 06:03AM: **Coq datatype - pair of pair with bracket – stackoverflow.com**

**Y.X.** posted a new question on June 28, 2021 at 12:03PM: **How does the "intro ->" in Coq work on context? – stackoverflow.com**

**steve01** posted a new question on June 30, 2021 at 08:56PM: **Why simultaneous assignment fails? – stackoverflow.com**

**joshan beha** posted a new question on July 02, 2021 at 05:56PM: **How to consider both out puts in list – stackoverflow.com**

**user12986714** posted a new question on July 04, 2021 at 06:08AM: **Proving equivalence of two rev_append implementations – stackoverflow.com**

**leonaden** posted a new question on July 04, 2021 at 06:32AM: **Coq: Comparing an Int to a Nat in Separation Logic Foundations – stackoverflow.com**

**joshan beha** posted a new question on July 04, 2021 at 06:52PM: **Elements count in list – stackoverflow.com**

**Serene** posted a new question on July 07, 2021 at 05:53AM: **How can I replace a variable by another in coq – stackoverflow.com**

**12412316** posted a new question on July 08, 2021 at 07:00AM: **Can any additional axiom make Coq Turing complete? – stackoverflow.com**

**DoubleX** posted a new question on July 08, 2021 at 07:03AM: **How to clear duplicated hypothesis in Coq? – stackoverflow.com**

**DoubleX** posted a new question on July 08, 2021 at 07:03AM: **How to group duplicated hypothesis in Coq? – stackoverflow.com**

**Hexirp** posted a new question on July 09, 2021 at 06:07PM: **I tried to use PHOAS in Coq to formalize a calculus with full dependent types – stackoverflow.com**

**Night Heron** posted a new question on July 10, 2021 at 08:45AM: **Frama-C 23 and Coq – stackoverflow.com**

**joshan beha** posted a new question on July 10, 2021 at 06:12PM: **Proof related to list function – stackoverflow.com**

**joshan beha** posted a new question on July 10, 2021 at 06:12PM: **How to avoid true=false condition – stackoverflow.com**

**Feryll** posted a new question on July 11, 2021 at 05:07AM: **Coq: Induction on associated variable – stackoverflow.com**

**Serene** posted a new question on July 11, 2021 at 12:37PM: **How can I replace a variable by another in coq – mathoverflow.net**

**joshan beha** posted a new question on July 11, 2021 at 07:14PM: **equality of two numbers – stackoverflow.com**

**Benjamin Bray** posted a new question on July 14, 2021 at 02:16PM: **Coq match on Hypothesis passed to Ltac tactic – stackoverflow.com**

**Finn** posted a new question on July 16, 2021 at 02:14PM: **Why does Coquelicot mess with my bullets? – stackoverflow.com**

**aleesha zee** posted a new question on July 18, 2021 at 02:46PM: **Detail of Stack overflow questions – stackoverflow.com**

**Wonil Lee** posted a new question on July 21, 2021 at 08:18AM: **Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_" – stackoverflow.com**

**Sereja Bogolubov** posted a new question on July 21, 2021 at 06:49PM: **Coq + Emacs? Check can't see what is defined in the source file – stackoverflow.com**

**Serene** posted a new question on July 21, 2021 at 10:34PM: **Proving an addition function is associative using Coq – stackoverflow.com**

**Dave Walker** posted a new question on July 23, 2021 at 01:02PM: **Proving two functions are equivalent without exactly the same hypotheses – stackoverflow.com**

**FH35** posted a new question on July 24, 2021 at 04:24PM: **How to use a theorem with a match pattern – stackoverflow.com**

**Sereja Bogolubov** posted a new question on July 27, 2021 at 09:13PM: **Coq: proving P -> ~P -> Q without contradiction tactic? – stackoverflow.com**

**Hexirp** posted a new question on July 28, 2021 at 05:41PM: **Can I define an equivalent to this using the Axiom command? – stackoverflow.com**

**sara lee** posted a new question on August 01, 2021 at 08:22AM: **Use of recursive function in Coq – stackoverflow.com**

**zoha ze** posted a new question on August 07, 2021 at 06:20AM: **How to represent mathematical function in coq – stackoverflow.com**

**ZhangLiao** posted a new question on August 07, 2021 at 09:18AM: **A question implement CPS transform in COq – cstheory.stackexchange.com**

**c_j_blank** posted a new question on August 09, 2021 at 07:35AM: **Joining trees together to create a new tree - Coq – stackoverflow.com**

**Sereja Bogolubov** posted a new question on August 11, 2021 at 05:06PM: **Coq: eliminating forall? – stackoverflow.com**

**user251130** posted a new question on August 18, 2021 at 05:46PM: **Making coercions explicit in assumptions in Coq – stackoverflow.com**

**Pedro Queiroga** posted a new question on August 18, 2021 at 07:53PM: **How to apply in many hypothesis at once? – stackoverflow.com**

**Vadim Pushtaev** posted a new question on August 18, 2021 at 09:21PM: **Destruct hypothesis: general case – stackoverflow.com**

**user1953221** posted a new question on August 21, 2021 at 07:46AM: **Proving equivalence of two programs expressed as different relations – stackoverflow.com**

**user1953221** posted a new question on August 21, 2021 at 07:46AM: **Proving equivalence of two programs expressed as different types – stackoverflow.com**

**exchange** posted a new question on August 22, 2021 at 01:01PM: **Is flattening a list easier in dependently typed functional programming languages? – stackoverflow.com**

**Shiranai** posted a new question on August 24, 2021 at 06:49PM: **Idempotency of normalizing a binary number in coq – stackoverflow.com**

**ZhangLiao** posted a new question on August 25, 2021 at 07:35PM: **How to know the number of isomorphisms in formal libraries? – cstheory.stackexchange.com**

**Hexirp** posted a new question on August 26, 2021 at 08:12AM: **Can I prove "coinductive principles" about coinductive type? – stackoverflow.com**

**ZhangLiao** posted a new question on August 27, 2021 at 02:02PM: **Is there a formal libray can show how many times a specified symbols appear in the library? – cstheory.stackexchange.com**

**santker heboln** posted a new question on August 27, 2021 at 08:43PM: **Definition of Category and internal category in coq – stackoverflow.com**

**Henry Zhang** posted a new question on August 31, 2021 at 01:43AM: **In Coq how to combine two hypothesis or rearrange the parenthesis in subgoals – stackoverflow.com**

**Grant Jurgensen** posted a new question on September 01, 2021 at 12:16AM: **Why can't Coq infer my coercion when applying arguments to coercible term? – stackoverflow.com**

**pjm** posted a new question on September 02, 2021 at 06:50PM: **Combine implicit arguments and partial application – stackoverflow.com**

**scubed** posted a new question on September 05, 2021 at 08:05AM: **The missing De Morgan's law – stackoverflow.com**

**user566206** posted a new question on September 05, 2021 at 04:27PM: **How can I prove add_le_cases (forall n m p q, n + m <= p + q -> n <= p \/ m <= q) – stackoverflow.com**

**NotAPlane** posted a new question on September 05, 2021 at 10:20PM: **New to Coq: How to compile .vo files and run command line? – stackoverflow.com**

**Andrew Au** posted a new question on September 07, 2021 at 12:26AM: **Annotating Coq proofs – stackoverflow.com**

**Andrey** posted a new question on September 07, 2021 at 09:42AM: **What the data type does author mean in exercises for cpdt book? – stackoverflow.com**

**Kristian** posted a new question on September 08, 2021 at 12:17PM: **Adding "in" part to tactic to specify where to apply it – stackoverflow.com**

**Abastro** posted a new question on September 08, 2021 at 02:49PM: **Proof irrelevance of decidable *inequality* in coq – stackoverflow.com**

**Serene M** posted a new question on September 08, 2021 at 02:53PM: **How to prove list concatenation is not commutative using coq? – stackoverflow.com**

**Serene M** posted a new question on September 09, 2021 at 12:56AM: **Error message: Not the right number of missing arguments (expected 1) – stackoverflow.com**

**Kristian** posted a new question on September 11, 2021 at 12:48AM: **Problems with missing information in Obligations when defining using Program in Coq – stackoverflow.com**

**user566206** posted a new question on September 11, 2021 at 05:21PM: **Proving MStar' in Logical Foundations (IndProp.v) – stackoverflow.com**

**Serene M** posted a new question on September 13, 2021 at 02:20AM: **An assumption in the goal is completely the same with a function I defined beforehand. How can I tell Coq they are indeed the same? – stackoverflow.com**

**Kristian** posted a new question on September 13, 2021 at 08:49PM: **Add notation to a scope globally in Coq – stackoverflow.com**

**Felipe Balbi** posted a new question on September 13, 2021 at 08:52PM: **Binary tree inversion in Coq – stackoverflow.com**

**Fusen** posted a new question on September 15, 2021 at 10:33AM: **VSCoq ProofView not printing – stackoverflow.com**

**Andrey** posted a new question on September 16, 2021 at 04:10PM: **ssreflect inversion, I need two equations instead of one – stackoverflow.com**

**paulotorrens** posted a new question on September 17, 2021 at 10:20PM: **Is it possible to turn unification errors into goals in Coq? – stackoverflow.com**

**Rupert Swarbrick** posted a new question on September 20, 2021 at 12:40AM: **Trying to define a "rect2"-like function on heterogeneous vectors – stackoverflow.com**

**Serene M** posted a new question on September 20, 2021 at 07:09AM: **Error: Cannot interpret this number as a value of type nat – stackoverflow.com**

**Felipe Balbi** posted a new question on September 20, 2021 at 07:56AM: **Software Foundations Volume 1: Tactics: injection_ex3 – stackoverflow.com**

**KaisoHHH** posted a new question on September 21, 2021 at 06:33AM: **Coq proof for a regular expression on boolean value – stackoverflow.com**

**Kristian** posted a new question on September 23, 2021 at 12:58PM: **Avoid dulicating code for applying tactics in both hypothesis and goal – stackoverflow.com**

**Kristian** posted a new question on September 23, 2021 at 12:58PM: **Avoid duplicating code for applying tactics in both hypothesis and goal – stackoverflow.com**

**Grant Jurgensen** posted a new question on September 24, 2021 at 10:56PM: **How does axiom K contradict univalence? – cstheory.stackexchange.com**

**geckos** posted a new question on September 25, 2021 at 06:42PM: **How to generalize a variable on both sides of an equation in Coq? – stackoverflow.com**

**Jan Tušil** posted a new question on September 27, 2021 at 11:40AM: **Coq unshelve in LTac2 – stackoverflow.com**

**Jason Gross** posted a new question on September 27, 2021 at 07:17PM: **Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)? – stackoverflow.com**

**dd21** posted a new question on September 27, 2021 at 09:11PM: **how to prove x + n = y + n -> x = y in coq – stackoverflow.com**

**azani** posted a new question on September 28, 2021 at 03:01AM: **Can't figure out why re-write does not work – stackoverflow.com**

**Felipe Balbi** posted a new question on September 28, 2021 at 01:32PM: **SF Volume 1: Logic: How to prove tr_rev <-> rev? – stackoverflow.com**

**Felipe Balbi** posted a new question on September 29, 2021 at 12:17PM: **How to split equality of two lists? – stackoverflow.com**

**Tyler's ruler** posted a new question on October 01, 2021 at 04:32PM: **How to prove this DeMorgan law without using automation tactics in Coq? – stackoverflow.com**

**Felipe Balbi** posted a new question on October 01, 2021 at 07:17PM: **How to tell Coq that it's okay to remove the ns? – stackoverflow.com**

**OrenIshShalom** posted a new question on October 02, 2021 at 06:52AM: **Equal implies Less-Than-Or-Equal in Coq – stackoverflow.com**

**azani** posted a new question on October 02, 2021 at 08:23PM: **How can I get C-c C-n to format the current line in proof-general coq-mode-map – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 03, 2021 at 05:54PM: **Suppress Warning At Import – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 04, 2021 at 09:21AM: **Coercion in pairs – stackoverflow.com**

**sweetieeee** posted a new question on October 04, 2021 at 10:49AM: **What does the tactic destruct do in the proof below? – stackoverflow.com**

**Felipe Balbi** posted a new question on October 04, 2021 at 11:42AM: **How to prove plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. – stackoverflow.com**

**Felipe Balbi** posted a new question on October 05, 2021 at 02:03PM: **How to prove Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m – stackoverflow.com**

**Matthew Gregoire** posted a new question on October 05, 2021 at 10:23PM: **How to express that one element of an inductive relation can't be derived from another in Coq? – stackoverflow.com**

**Sami Liedes** posted a new question on October 06, 2021 at 12:05AM: **Weird goal Some 0 = true generated in proof – stackoverflow.com**

**inmessionante** posted a new question on October 06, 2021 at 01:00AM: **proof tactics in coq can replace inversion – stackoverflow.com**

**Bob** posted a new question on October 07, 2021 at 10:29AM: **Not pretty-printing a field of a record – stackoverflow.com**

**Felipe Balbi** posted a new question on October 10, 2021 at 04:08PM: **Software Foundations: weak_pumping lemma proof – stackoverflow.com**

**chen yu** posted a new question on October 12, 2021 at 02:57PM: **Can any one help me how to prove this therom in coq – stackoverflow.com**

**dkutlesic** posted a new question on October 13, 2021 at 03:17PM: **COQ: How to use "<=" for Z and R in the same lemma? – stackoverflow.com**

**geckos** posted a new question on October 16, 2021 at 11:50PM: **How to apply an axiom to simplify a match in Coq? – stackoverflow.com**

**Chloe** posted a new question on October 17, 2021 at 08:28PM: **Coq stuck on proof for Theorem eqblist_true – cs.stackexchange.com**

**ged** posted a new question on October 18, 2021 at 04:35PM: **Proving that s-expressions printing is injective – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 19, 2021 at 03:04PM: **Coercions of bitvectors – stackoverflow.com**

**qbn qsj** posted a new question on October 19, 2021 at 05:45PM: **Proof in Coq with named parameters in constructors – stackoverflow.com**

**Audition** posted a new question on October 20, 2021 at 03:50PM: **Coq Error: Illegal application (Non-functional construction) – stackoverflow.com**

**geckos** posted a new question on October 21, 2021 at 04:03AM: **How to do induction on BinNums.Z in Coq/ – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 21, 2021 at 10:33AM: **Why does an "only printing" notation modify the parser – stackoverflow.com**

**Bruno** posted a new question on October 23, 2021 at 12:39AM: **Real numbers in Coq – stackoverflow.com**

**Kristian** posted a new question on October 25, 2021 at 05:03PM: **Decidable equality statement with Set vs. Prop – stackoverflow.com**

**dkutlesic** posted a new question on October 27, 2021 at 02:25PM: **COQ: a_j <= b_j => sum (a_j) <= sum (b_j) – stackoverflow.com**

**dkutlesic** posted a new question on October 27, 2021 at 02:25PM: **Proving a_j ≤ b_j → sum (a_j) ≤ sum (b_j) – stackoverflow.com**

**Vaishnavi Lakkalkatti ee17b065** posted a new question on October 28, 2021 at 11:35AM: **Modulo simplification in coq – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 29, 2021 at 09:51AM: **Implicit parameter in singleton class – stackoverflow.com**

**Grant Jurgensen** posted a new question on October 29, 2021 at 09:21PM: **Is CoInductive "extensionality" sound in Coq? Is it generalizable? – stackoverflow.com**

**Proof-By-Sledgehammer** posted a new question on October 30, 2021 at 10:56AM: **state monad on field of record – stackoverflow.com**

**Sebastian Fisher** posted a new question on November 01, 2021 at 02:30PM: **Transitivity of subsequence in COQ – stackoverflow.com**

**pjm** posted a new question on November 02, 2021 at 06:11PM: **Coinductive principle for streams – stackoverflow.com**

**LogicChains** posted a new question on November 03, 2021 at 07:48AM: **Is "less than" for rational numbers decideable in Coq? – stackoverflow.com**

**joro** posted a new question on November 03, 2021 at 10:12AM: **Can we get contradiction in ZFC if we define $a\mod 0$? – mathoverflow.net**

**sdpoll** posted a new question on November 05, 2021 at 10:27PM: **How to try a tactic in Ltac, but continue if it fails – stackoverflow.com**

**sdpoll** posted a new question on November 05, 2021 at 10:57PM: **What is the tactic that does nothing? – stackoverflow.com**

**geckos** posted a new question on November 07, 2021 at 09:08PM: **What is the difference of induction n, m and induction n; induction m in Coq? – stackoverflow.com**

**nanoeng** posted a new question on November 09, 2021 at 04:09AM: **What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu? – stackoverflow.com**

**John Regis** posted a new question on November 10, 2021 at 06:41PM: **Coq: How to prove that forall n m, n <= m \/ m <= n – stackoverflow.com**

**ged** posted a new question on November 11, 2021 at 01:10PM: **Unification problem with HOL-style alpha-conversion in Coq (matching the equality) – stackoverflow.com**

**Damián Ferencz** posted a new question on November 12, 2021 at 03:05PM: **Is it possible to declare type-dependent Notation in Coq? – stackoverflow.com**

**sdpoll** posted a new question on November 12, 2021 at 10:57PM: **How to replace a term with some property of the term? – stackoverflow.com**

**მამუკა ჯიბლაძე** posted a new question on November 13, 2021 at 05:46PM: **Coq seemingly refuses to recognize a simple substitution of a propositional formula for a propositional variable? – stackoverflow.com**

**calcert** posted a new question on November 15, 2021 at 05:27PM: **Certified calculations in a proof assistant – stackoverflow.com**

**Sebastian Fisher** posted a new question on November 17, 2021 at 04:04AM: **Is there a more elegant way to convince coq that a list based hypothesis is a contradiction? – stackoverflow.com**

**Walter Schulze** posted a new question on November 17, 2021 at 09:03AM: **Mutually Recursive Function to Compare Trees – stackoverflow.com**

**sdpoll** posted a new question on November 17, 2021 at 08:46PM: **How does the Info vernacular command work? – stackoverflow.com**

**sdpoll** posted a new question on November 17, 2021 at 10:11PM: **How can I reorder existential variables in Coq? – stackoverflow.com**

**Dan Arnon** posted a new question on November 19, 2021 at 11:25PM: **Why does Coq restrict Inductive-Recursive definitions, and how is this related to Inaccessible cardinals? – mathoverflow.net**

**Dan Arnon** posted a new question on November 19, 2021 at 11:25PM: **Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals? – mathoverflow.net**

**Ember Edison** posted a new question on November 20, 2021 at 05:59PM: **constructive Scott's trick – stackoverflow.com**

**Musher Soccoli** posted a new question on November 23, 2021 at 04:20PM: **Equality between two propositions nat -> nat – stackoverflow.com**

**Musher Soccoli** posted a new question on November 23, 2021 at 06:06PM: **Good way of testing a class in Coq – stackoverflow.com**

**Jan Tušil** posted a new question on November 24, 2021 at 09:24PM: **Controlling unification order in Coq – stackoverflow.com**

**Musher Soccoli** posted a new question on November 25, 2021 at 03:33PM: **Difference between parameters and conditions of a class – stackoverflow.com**

**Musher Soccoli** posted a new question on November 25, 2021 at 03:33PM: **Difference between parameters and members of a class – stackoverflow.com**

**მამუკა ჯიბლაძე** posted a new question on November 28, 2021 at 06:56AM: **Coq: a vicious circle with two identical subgoals – stackoverflow.com**

**John Regis** posted a new question on November 29, 2021 at 05:07PM: **Solving a split proof in Coq – stackoverflow.com**

**John Regis** posted a new question on November 29, 2021 at 07:30PM: **Select_perm' lemma – stackoverflow.com**

**Musher Soccoli** posted a new question on November 29, 2021 at 09:27PM: **Unable to split a conjunction in Hypothesis – stackoverflow.com**

**Musher Soccoli** posted a new question on November 30, 2021 at 07:02PM: **How to proove that all elements in a list are smaller than a given element in coq – stackoverflow.com**

**geckos** posted a new question on December 01, 2021 at 12:53AM: **How can I proove 0 <= a < b -> rem a b = a in Coq? – stackoverflow.com**

**Musher Soccoli** posted a new question on December 01, 2021 at 09:36PM: **Proving existance by providing an example – stackoverflow.com**

**Musher Soccoli** posted a new question on December 02, 2021 at 06:41PM: **Proof with multiple cases theorem – stackoverflow.com**

**Abcdef** posted a new question on December 05, 2021 at 07:02PM: **Issue with setting up Coq on VScode, "You don't have an extension for debugging Coq" – stackoverflow.com**

**Huan Sun** posted a new question on December 08, 2021 at 01:21PM: **can't launch CoqIde – stackoverflow.com**

**nanoeng** posted a new question on December 08, 2021 at 05:50PM: **Problems generating *.vos file due to CoQ Tatic failure (reversible 1st order mode) and wrong bullet – stackoverflow.com**

**Huan Sun** posted a new question on December 09, 2021 at 03:09AM: **How to Import Coq library HoTT in CoqIde – stackoverflow.com**

**luke36** posted a new question on December 09, 2021 at 02:18PM: **Reversing a vector in Coq – stackoverflow.com**

**dgan** posted a new question on December 11, 2021 at 11:14PM: **Are those two proofs equivalent? – stackoverflow.com**

**Charlie Parker** posted a new question on December 12, 2021 at 04:02PM: **How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 using auto but in Coq? – stackoverflow.com**

**Musher Soccoli** posted a new question on December 15, 2021 at 02:07PM: **Minimum of an ensemble in Coq – stackoverflow.com**

**Musher Soccoli** posted a new question on December 15, 2021 at 02:07PM: **Minimum of a set in Coq – stackoverflow.com**

**Musher Soccoli** posted a new question on December 15, 2021 at 10:43PM: **Proof with forall for a particular term – stackoverflow.com**

**KingsAlpaca** posted a new question on December 16, 2021 at 10:58AM: **Coq: Associativity of relational composition – stackoverflow.com**

**Musher Soccoli** posted a new question on December 17, 2021 at 09:56AM: **Simplify negation of inequality – stackoverflow.com**

**Charlie Parker** posted a new question on December 17, 2021 at 04:35PM: **How does one produce types (or theorems) from proof terms (programs or objects) in Coq? – stackoverflow.com**

**Lepticed** posted a new question on December 17, 2021 at 11:03PM: **Is there a shorter proof to this Coq theorem? – stackoverflow.com**

**Lepticed** posted a new question on December 18, 2021 at 11:32AM: **Proving a theorem containing not exists – stackoverflow.com**

**sdpoll** posted a new question on December 21, 2021 at 08:03AM: **What does the term "?T@{x:=t}", or a type with a question mark and at sign surrounding it mean in Coq? – stackoverflow.com**

**Charlie Parker** posted a new question on December 21, 2021 at 08:15PM: **What is the runtime/time complexity of Coq’s (Dependent) Type Inference? – cs.stackexchange.com**

**user615297** posted a new question on December 21, 2021 at 11:01PM: **Supply exist argument COQ – stackoverflow.com**

**Grant Jurgensen** posted a new question on December 22, 2021 at 04:39PM: **Why is UIP unprovable in Coq? Why does the match construct generalize types? – stackoverflow.com**

**user1953221** posted a new question on December 25, 2021 at 09:52AM: **Trace inclusion between program and state machine – stackoverflow.com**

**Jeff Li** posted a new question on December 25, 2021 at 11:17AM: **How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))? – stackoverflow.com**

**Paprika** posted a new question on December 25, 2021 at 10:57PM: **Understanding the intros keyword work in Coq – stackoverflow.com**

**dgan** posted a new question on December 27, 2021 at 12:59AM: **Cannot rewrite goal with assertion? – stackoverflow.com**

**Paprika** posted a new question on December 27, 2021 at 01:40AM: **Proving S (n + m) = n + (S m), how to rewrite n+1 = S(n)? – stackoverflow.com**

**geckos** posted a new question on December 28, 2021 at 04:05PM: **How can I proove forall a b, a <=? b = true -> a <=? S b = true) – stackoverflow.com**

**Rabbit Angstrom** posted a new question on December 28, 2021 at 08:54PM: **Coq & Emacs: Cannot compile Coq - No such file or directory – stackoverflow.com**

**geckos** posted a new question on December 28, 2021 at 04:05PM: **How can I proove forall a b, a <=? b = true -> a <=? S b = true in Coq – stackoverflow.com**

**Huan Sun** posted a new question on December 29, 2021 at 03:55AM: **How to understand syntax engine in Isabelle – stackoverflow.com**

**Mervin Macky** posted a new question on January 01, 2022 at 12:53PM: **Coq's proof #Coq – stackoverflow.com**

**geckos** posted a new question on January 05, 2022 at 02:35PM: **Is it possible to import a file in a proof only in Coq? – stackoverflow.com**

**The_Ghost** posted a new question on January 06, 2022 at 01:36PM: **How to prove shorter nat comparisons like 10000 > 1 for sigma types in Coq? – stackoverflow.com**

**sdpoll** posted a new question on January 08, 2022 at 01:17AM: **How can I write a tactic which works both in a goal and a hypothesis? – stackoverflow.com**

**Natasha Klaus** posted a new question on January 08, 2022 at 06:36AM: **Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen) – stackoverflow.com**

**Yu-zh** posted a new question on January 13, 2022 at 07:31AM: **Relations with dependent types in Coq – stackoverflow.com**

**Ramtin** posted a new question on January 14, 2022 at 07:33PM: **Why Coq does not infer the type parameter – stackoverflow.com**

**Sambo** posted a new question on January 15, 2022 at 11:55PM: **Coq - Coercion of list nat – stackoverflow.com**

**LittleJian** posted a new question on January 18, 2022 at 09:56AM: **How to prove the correction of derive on reg_exp – stackoverflow.com**

**Ene** posted a new question on January 20, 2022 at 04:41AM: **Defining functions on non-inductive types using LEM in Coq – cstheory.stackexchange.com**

**Breno** posted a new question on January 20, 2022 at 07:58PM: **How to prove an absurd rule in Coq – stackoverflow.com**

**Jimmy Stone** posted a new question on January 23, 2022 at 04:09AM: **Check cnat. and got Type return – stackoverflow.com**

**Roberto Ierusalimschy** posted a new question on January 23, 2022 at 02:29PM: **Coq: trying to use dependent induction – stackoverflow.com**

**Sam Li** posted a new question on January 23, 2022 at 03:02PM: **Addition of natural numbers in Coq – stackoverflow.com**

**IsAdisplayName** posted a new question on January 24, 2022 at 02:47AM: **Problem with Ocaml and make: "Error: the file ____.cmxa is not a compilation unit description" – stackoverflow.com**

**Breno** posted a new question on January 27, 2022 at 04:45PM: **How to prove in Coq ~~(P \/ ~P) – stackoverflow.com**

**user615297** posted a new question on January 27, 2022 at 09:46PM: **Coq, true datatype – stackoverflow.com**

**french_cruller** posted a new question on January 28, 2022 at 02:16PM: **Proof of "less equal" transitive law in Coq – stackoverflow.com**

**Hexirp** posted a new question on January 29, 2022 at 09:20AM: **In Coq, Export, Require, and filtered_import do not work well – stackoverflow.com**

**IsAdisplayName** posted a new question on January 29, 2022 at 09:56PM: **Problems adding new notation in Coq – stackoverflow.com**

**Sambo** posted a new question on February 01, 2022 at 08:14PM: **Coq - Obtaining equality from match statement – stackoverflow.com**

**IsAdisplayName** posted a new question on February 03, 2022 at 08:03AM: **Coq rewrite tactic can't find subterm – stackoverflow.com**

**user615297** posted a new question on February 05, 2022 at 02:15PM: **Apply and apply with COQ – stackoverflow.com**

**Brent Pappas** posted a new question on February 05, 2022 at 03:09PM: **Coq - Rewriting a FMap Within a Relation – stackoverflow.com**

**dgan** posted a new question on February 05, 2022 at 07:13PM: **Coq: Cannot infer an internal placeholder of type "nat" in environment: ev : nat -> Prop – stackoverflow.com**

**IsAdisplayName** posted a new question on February 07, 2022 at 08:34PM: **Coq: How are the equality tacticts symmetry and transitivity defined? – stackoverflow.com**

**IsAdisplayName** posted a new question on February 07, 2022 at 08:52PM: **Coq Uni Math Sigma Types Wont Bind a family of types – stackoverflow.com**

**Ak_Ak** posted a new question on February 08, 2022 at 03:38PM: **Theorem euclid_gcd , proving that forall a b z, euclid a b z -> gcd a b z. using coq – stackoverflow.com**

**Breno** posted a new question on February 11, 2022 at 05:23PM: **How to prove that another definition of permutation is the same as the Default Permutation Library for COQ – stackoverflow.com**

**Charlie Parker** posted a new question on February 14, 2022 at 09:20PM: **How does one install a new version of Coq when it cannot find the repositories in a new mac m1 machine? – stackoverflow.com**

**nobody** posted a new question on February 16, 2022 at 03:06PM: **Best practices for parametrized Coq libraries – stackoverflow.com**

**dgan** posted a new question on February 18, 2022 at 08:33PM: **"False" in goal: is that a an indication I am doing something wrong? – stackoverflow.com**

**Ricardo Maurizio Paul** posted a new question on February 21, 2022 at 01:41PM: **Coq: prove while is equivalent to repeat – stackoverflow.com**

**Sambo** posted a new question on February 21, 2022 at 10:27PM: **Coq: goal is just a type (when using theorems with unnecessary arguments) – stackoverflow.com**

**georgionic** posted a new question on February 22, 2022 at 02:59PM: **How to create a Powerset of MSetList? – stackoverflow.com**

**Jo Liss** posted a new question on February 22, 2022 at 03:15PM: **How to run SearchAbout snippet in company-coq-tutorial – stackoverflow.com**

**Jo Liss** posted a new question on February 22, 2022 at 11:18PM: **Remove useless hypothesis from context – stackoverflow.com**

**Natasha Klaus** posted a new question on February 24, 2022 at 11:32AM: **Problem with Dependent pattern matching in COQ – stackoverflow.com**

**7Orion7** posted a new question on February 25, 2022 at 03:39PM: **Why does this Coq Definition fail? Coq Namespace error for Inductive Type – stackoverflow.com**

**Jimmy Stone** posted a new question on February 26, 2022 at 01:24PM: **Translate smtlib2 model to COQ – stackoverflow.com**

**Jo Liss** posted a new question on February 26, 2022 at 03:51PM: **Curly brace proof syntax: begin x. = { auto } y. [] – stackoverflow.com**

**Jo Liss** posted a new question on February 28, 2022 at 01:27PM: **Tactic for existential hypothesis – stackoverflow.com**

**nss** posted a new question on March 01, 2022 at 09:24PM: **how do I prove forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) ->Q. in coq? – stackoverflow.com**

**Alex Nicolaou** posted a new question on March 02, 2022 at 03:00AM: **What causes fix to appear after unfolding? – stackoverflow.com**

**John Targaryen** posted a new question on March 03, 2022 at 12:22AM: **coq: Tactic to replace true hypothesis in 'and' statement – stackoverflow.com**

**Felipe Balbi** posted a new question on March 03, 2022 at 09:13PM: **Proving Binary Tree Properties – stackoverflow.com**

**Charlie Parker** posted a new question on March 03, 2022 at 09:28PM: **How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop)) – stackoverflow.com**

**Charlie Parker** posted a new question on March 04, 2022 at 03:11PM: **How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq? – stackoverflow.com**

**Charlie Parker** posted a new question on March 04, 2022 at 03:18PM: **What do the consecutive in's in Coq do and eval & red & Idtac do? – stackoverflow.com**

**Charlie Parker** posted a new question on March 04, 2022 at 06:44PM: **How does one automatically lint Coq files in vscode? – stackoverflow.com**

**Huan Sun** posted a new question on March 05, 2022 at 03:18PM: **Is there a way to apply the rule to a specific assumption in Isabelle? – stackoverflow.com**

**Alex Nicolaou** posted a new question on March 07, 2022 at 03:16PM: **Proving weaker exists based on forall – stackoverflow.com**

**Charlie Parker** posted a new question on March 08, 2022 at 01:04AM: **What does apply. tactic on it's own do in Coq -- i.e. without specifying a rule or hypothesis to unify the goal's conclusion with? – stackoverflow.com**

**Charlie Parker** posted a new question on March 08, 2022 at 02:18AM: **What is the right proof term so that the ssreflect tutorial work with the exact: hAiB example? – stackoverflow.com**

**Charlie Parker** posted a new question on March 09, 2022 at 12:51AM: **Why is my local coq no acting the same as standard coq e.g. as JsCoq? – stackoverflow.com**

**Charlie Parker** posted a new question on March 10, 2022 at 09:43PM: **Why does Coq remove/clear my asserted lemmas in my proof after the base case is proved? – stackoverflow.com**

**Sambo** posted a new question on March 11, 2022 at 07:52PM: **Creating Coq tactic: how to use a newly generated name? – stackoverflow.com**

**Kevin Flowers Jr** posted a new question on March 12, 2022 at 12:49AM: **Building non-classical logics in Adga & Coq – cs.stackexchange.com**

**F1r09** posted a new question on March 12, 2022 at 05:45PM: **how to create a polymorphe couple such as "( a : type A, b : type B ) " in lambda-calculus – stackoverflow.com**

**Vincent Iampietro** posted a new question on March 13, 2022 at 06:47PM: **How to tell the Coq kernel that a parameter of a lambda function is a subterm of another variable in the scope? – stackoverflow.com**

**F1r09** posted a new question on March 14, 2022 at 03:21PM: **Number of element in a list in lambd-calculus? – stackoverflow.com**

**F1r09** posted a new question on March 14, 2022 at 08:41PM: **Concatenation of 2 lists in lambda-calculus – stackoverflow.com**

**Echo_Zero** posted a new question on March 15, 2022 at 12:46PM: **Warning : “Set this option from the IDE menu instead” in coq – stackoverflow.com**

**lyfeng** posted a new question on March 10, 2022 at 05:18AM: **How to set defaults for implicit arguments when they can't be inferred? – proofassistants.stackexchange.com**

**Gregory Nisbet** posted a new question on March 12, 2022 at 02:22AM: **List of general purpose Coq sublanguages for defining custom tactics – proofassistants.stackexchange.com**

**Walter Schulze** posted a new question on March 14, 2022 at 09:05AM: **Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms – proofassistants.stackexchange.com**

**t1kumi** posted a new question on March 15, 2022 at 08:35PM: **reverse and insert list lambda calculus – stackoverflow.com**

**Kyrene** posted a new question on March 16, 2022 at 01:56AM: **How to prove a constant function that neither injective nor surjective in Coq? – stackoverflow.com**

**t1kumi** posted a new question on March 15, 2022 at 08:35PM: **How to reverse a list and insert an element in a list in lambda calculus? – stackoverflow.com**

**t1kumi** posted a new question on March 16, 2022 at 11:50AM: **How to reverse list in lambda calculus? – stackoverflow.com**

**ARevX** posted a new question on March 17, 2022 at 02:52PM: **Coq proof usage – stackoverflow.com**

**Théo Winterhalter** posted a new question on March 17, 2022 at 08:00PM: **Well-foundedness: classical equivalence of no infinite descent and accessibility – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on March 17, 2022 at 08:26PM: **How does one define dependent type with named arguments in Coq without issues in unification in the constructors? – stackoverflow.com**

**Charlie Parker** posted a new question on March 17, 2022 at 09:16PM: **How does one build the list of only true elements in Coq using dependent types? – stackoverflow.com**

**Kevin Flowers Jr** posted a new question on March 12, 2022 at 12:49AM: **Building non-classical logics in Agda & Coq – cs.stackexchange.com**

**Kyle Stemen** posted a new question on March 18, 2022 at 11:48AM: **For functions that are eq_dep equal, are their applications eq_dep equal without axioms? – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on March 18, 2022 at 07:35PM: **What does IH cannot be used as a hint. in Coq mean when using eauto giving it the induction hypothesis directly? – stackoverflow.com**

**Nicholas Weston** posted a new question on March 19, 2022 at 09:02AM: **Removing the last element of a sized list in Coq – stackoverflow.com**

**t1kumi** posted a new question on March 19, 2022 at 11:34AM: **Determine if a given tree is a binary search tree with lambda calculus – stackoverflow.com**

**Charlie Parker** posted a new question on March 19, 2022 at 03:41PM: **How to solve the very simple Syntax error: 'end' expected after [branches] (in [term_match]). in Coq? (in Gallina and not ltac) – stackoverflow.com**

**Jason Rute** posted a new question on March 19, 2022 at 09:59PM: **How does the formal proof of the four color theorem work? – proofassistants.stackexchange.com**

**Josip Pavičić** posted a new question on March 20, 2022 at 12:19PM: **proving surjectivity in coq – stackoverflow.com**

**Kyrene** posted a new question on March 23, 2022 at 07:39PM: **Proof constant not surjective Coq – stackoverflow.com**

**Molossus Spondee** posted a new question on March 23, 2022 at 08:56PM: **How to write heavily indexed proofs? – proofassistants.stackexchange.com**

**Carl Patenaude Poulin** posted a new question on March 24, 2022 at 12:16AM: **Coq: what does it mean to "saturate" a proof's context? – stackoverflow.com**

**Carl Patenaude Poulin** posted a new question on March 24, 2022 at 12:28AM: **Coq: easiest way to construct members of a decidable sigma type? – stackoverflow.com**

**Sebastian Fisher** posted a new question on March 24, 2022 at 08:04PM: **Coq Program Fixpoint vs equations as far as best way to get reduction lemmas? – stackoverflow.com**

**Breno** posted a new question on March 26, 2022 at 01:20AM: **How to build a proof of correctness in coq for elements_tr – stackoverflow.com**

**Breno** posted a new question on March 27, 2022 at 04:40AM: **How to prove insert_BST in Coq – stackoverflow.com**

**q.undertow** posted a new question on March 27, 2022 at 07:26PM: **Why does this trivial prrof fail with structuring tacticals? – proofassistants.stackexchange.com**

**q.undertow** posted a new question on March 27, 2022 at 07:26PM: **Why does this trivial proof fail with structuring tacticals? – proofassistants.stackexchange.com**

**Ende Jin** posted a new question on March 29, 2022 at 09:49PM: **Does Coq's Module and Functor type-check incrementally? – proofassistants.stackexchange.com**

**nss** posted a new question on March 30, 2022 at 12:40AM: **I am trying to solve constant is not surjective through coq – stackoverflow.com**

**Couchy** posted a new question on March 31, 2022 at 07:40PM: **What is the role of impredicativity in program extraction? – proofassistants.stackexchange.com**

**Breno** posted a new question on April 01, 2022 at 04:13AM: **How to solve a simple inequality in COQ with the same variable which is adding on both sides of the inequality – stackoverflow.com**

**Lepticed** posted a new question on April 01, 2022 at 11:06AM: **Using the commutativity of the AND operator in Coq – stackoverflow.com**

**Lepticed** posted a new question on April 01, 2022 at 07:34PM: **Define a function based on a relation in Coq – stackoverflow.com**

**sdpoll** posted a new question on April 06, 2022 at 01:16AM: **Using tuples when constructing inductive types – stackoverflow.com**

**Lepticed** posted a new question on April 06, 2022 at 04:28PM: **Pose proof in Coq – stackoverflow.com**

**Lepticed** posted a new question on April 07, 2022 at 10:12PM: **How to get a better proof style in Coq? – stackoverflow.com**

**L. F.** posted a new question on April 09, 2022 at 03:07AM: **Proving uniqueness of an instance of an indexed inductive type – proofassistants.stackexchange.com**

**Ende Jin** posted a new question on April 11, 2022 at 09:25PM: **Why Coq's Include is designed to instantiate functor with current interactive defining module? – proofassistants.stackexchange.com**

**dvr** posted a new question on April 11, 2022 at 11:47PM: **rewriting hypothesis to false with a contradictory theorem – stackoverflow.com**

**Kevin Buzzard** posted a new question on April 12, 2022 at 02:53PM: **Examples of formalisation of abelian categories – proofassistants.stackexchange.com**

**Couchy** posted a new question on April 13, 2022 at 02:35AM: **Defining coercion for proof irrelevant equality – proofassistants.stackexchange.com**

**lyfeng** posted a new question on April 13, 2022 at 03:25AM: **How to provide a countType when using mathcomp? – proofassistants.stackexchange.com**

**Tempestas Ludi** posted a new question on April 13, 2022 at 02:11PM: **Cannot discriminate 0 = 1 – proofassistants.stackexchange.com**

**lyfeng** posted a new question on April 14, 2022 at 06:09PM: **How to prove has_esp when using mathcomp.analysis? – proofassistants.stackexchange.com**

**Andrey** posted a new question on April 15, 2022 at 11:52AM: **setoid_rewrite: rewrite under bindings with 2 parameters – stackoverflow.com**

**Guy Coder** posted a new question on April 15, 2022 at 01:34PM: **Can someone explain Coq math-comp repositories – proofassistants.stackexchange.com**

**louga31** posted a new question on April 15, 2022 at 05:02PM: **Problem proving a binary add function – proofassistants.stackexchange.com**

**Guy Coder** posted a new question on April 15, 2022 at 01:34PM: **Explanation of Coq math-comp repositories – proofassistants.stackexchange.com**

**lyfeng** posted a new question on April 14, 2022 at 06:09PM: **How can I prove has_esp when using mathcomp.analysis? – proofassistants.stackexchange.com**

**Ya Boi Spy7** posted a new question on April 16, 2022 at 08:02PM: **Unfolding a sum and making it match hypotheses – stackoverflow.com**

**louga31** posted a new question on April 16, 2022 at 09:24PM: **Coq: How to replace a function by it's body when making a proof – proofassistants.stackexchange.com**

**Alice** posted a new question on April 16, 2022 at 10:57PM: **Found a constructor of inductive type bool while a constructor of list is expected – stackoverflow.com**

**Alice** posted a new question on April 17, 2022 at 01:06AM: **How to do an inductive proof – stackoverflow.com**

**fyo** posted a new question on April 17, 2022 at 01:39PM: **Importing HoTT library in Coq – stackoverflow.com**

**Matty898** posted a new question on April 18, 2022 at 02:09AM: **How can I to prove this theorem through induction? – stackoverflow.com**

**Nova Sczerin** posted a new question on April 18, 2022 at 03:02AM: **How can I prove this theorem with induction in Coq? – proofassistants.stackexchange.com**

**Ben** posted a new question on April 16, 2022 at 09:24PM: **How to replace a function by its body – proofassistants.stackexchange.com**

**geckos** posted a new question on April 19, 2022 at 06:21AM: **How to dependent match on a list with two elements? – stackoverflow.com**

**Tempestas Ludi** posted a new question on April 19, 2022 at 01:21PM: **Found type UU where "?T" was expected – proofassistants.stackexchange.com**

**Alice** posted a new question on April 19, 2022 at 03:54PM: **proving a binary add function – stackoverflow.com**

**Alice** posted a new question on April 19, 2022 at 05:29PM: **how to code in coq a function that sum the integers represented by the 2 lists and boolean representing a holdback? – stackoverflow.com**

**Alice** posted a new question on April 19, 2022 at 10:15PM: **multiplication of two binary numbers – stackoverflow.com**

**DoubleX** posted a new question on April 20, 2022 at 12:32PM: **Coq Qed raise a warning with admitted lemmas – stackoverflow.com**

**Lepticed** posted a new question on April 20, 2022 at 01:52PM: **Using or_comm in Coq – stackoverflow.com**

**Alan Audia** posted a new question on April 20, 2022 at 09:31PM: **Proof by contradiction in Coq – stackoverflow.com**

**Tempestas Ludi** posted a new question on April 23, 2022 at 09:31AM: **Prove equality in a record type – proofassistants.stackexchange.com**

**Sacchan** posted a new question on April 24, 2022 at 12:23PM: **How to extract the witness from exists in Coq in function notation/without destructing? – proofassistants.stackexchange.com**

**HTNW** posted a new question on April 24, 2022 at 12:58PM: **What axioms do I need to search the naturals? – proofassistants.stackexchange.com**

**Herbal Tea** posted a new question on April 24, 2022 at 06:41PM: **How to exhaust the match with in coq using something like default or or clause? – stackoverflow.com**

**Herbal Tea** posted a new question on April 24, 2022 at 07:31PM: **in coq how to assume equality of two natural numbers – stackoverflow.com**

**Herbal Tea** posted a new question on April 25, 2022 at 02:12PM: **How can i model something with persistent state in coq? – stackoverflow.com**

**Attila Karoly** posted a new question on April 26, 2022 at 05:26PM: **How proof functions are combined in Coq – stackoverflow.com**

**Hoshino Tented** posted a new question on April 26, 2022 at 07:48PM: **In Coq, is there a way to prove a premise of a hypothesis conveniently? – stackoverflow.com**

**Attila Karoly** posted a new question on April 27, 2022 at 08:15AM: **Symbolic manipulation of terms in Coq – stackoverflow.com**

**Shubham Sondhi** posted a new question on April 27, 2022 at 04:23PM: **Adding an old version of Ocaml to Opam – stackoverflow.com**

**Rupert Swarbrick** posted a new question on April 28, 2022 at 12:09AM: **Searching for a counterexample to a decidable predicate – stackoverflow.com**

**mudri** posted a new question on April 28, 2022 at 10:46AM: **How do Coq's bidirectionality hints ( &) affect type checking? – proofassistants.stackexchange.com**

**Breno** posted a new question on April 29, 2022 at 06:32PM: **How to deal with division in COQ? – stackoverflow.com**

**azani** posted a new question on April 30, 2022 at 07:19PM: **How can I "specialize" a polymorphic type in Coq? – stackoverflow.com**

**mudri** posted a new question on April 30, 2022 at 07:31PM: **Tactic unification vs evarconv in Coq – proofassistants.stackexchange.com**

**Valdigleis** posted a new question on April 30, 2022 at 08:02PM: **Display style proofs using Coq – proofassistants.stackexchange.com**

**Max Kubierschky** posted a new question on May 01, 2022 at 03:23PM: **Calculus of (inductive) Constructions: Do inductive definitions increase proof strength? – mathoverflow.net**

**caio a** posted a new question on May 01, 2022 at 08:20PM: **Proof theorem about bst in coq – stackoverflow.com**

**Max Kubierschky** posted a new question on May 02, 2022 at 06:21AM: **Calculus of (inductive) Constructions: Do inductive definitions increase proof strength? – proofassistants.stackexchange.com**

**azani** posted a new question on May 02, 2022 at 09:12PM: **Why can I not apply f_equal to a hypothesis? – stackoverflow.com**

**hamid k** posted a new question on May 02, 2022 at 10:31PM: **Why coq doesn't use subtyping for logical or? – stackoverflow.com**

**FH35** posted a new question on May 03, 2022 at 08:30AM: **Precise control of conversion in Coq – stackoverflow.com**

**Shiranai** posted a new question on May 06, 2022 at 12:08AM: **Proof objects in the identity type – stackoverflow.com**

**Vladimir Karavaychuk** posted a new question on May 09, 2022 at 01:07PM: **Coq: Recursive notations with forall quantifier – stackoverflow.com**

**mobotsar** posted a new question on May 09, 2022 at 07:57PM: **I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq – proofassistants.stackexchange.com**

**FH35** posted a new question on May 10, 2022 at 01:31PM: **Proof on inductive type in Coq – stackoverflow.com**

**udduu** posted a new question on May 11, 2022 at 07:32PM: **How can i proof by absurd with coq? – stackoverflow.com**

**FH35** posted a new question on May 12, 2022 at 10:58AM: **Fail to rewrite list with app_removelast_last – stackoverflow.com**

**wdeweijer** posted a new question on May 13, 2022 at 03:48PM: **SSReflect tuple constructor: why not use phantom? – stackoverflow.com**

**hamid k** posted a new question on May 14, 2022 at 06:46PM: **Prove recursive function exists using only nat_ind – stackoverflow.com**

**wdeweijer** posted a new question on May 14, 2022 at 09:08PM: **SSReflect tuple constructor: why not use phantom? – proofassistants.stackexchange.com**

**Vladimir Prigodsky** posted a new question on May 14, 2022 at 09:09PM: **Unfolding expressions in Coq by one layer – proofassistants.stackexchange.com**

**Romain C** posted a new question on May 15, 2022 at 12:12AM: **Cannot apply one hypothesis to another – stackoverflow.com**

**Jimmy Stone** posted a new question on May 15, 2022 at 04:49AM: **Equivalence but not congruence – stackoverflow.com**

**monique** posted a new question on May 15, 2022 at 10:38PM: **Is it possible to check the length of two strings before pattern matching against them? – stackoverflow.com**

**FH35** posted a new question on May 17, 2022 at 11:01AM: **Fail to prove a permutation property – stackoverflow.com**

**Vladimir Prigodsky** posted a new question on May 17, 2022 at 07:47PM: **Coq: Recursive notations with forall quantifier – proofassistants.stackexchange.com**

**147pm** posted a new question on May 19, 2022 at 05:17AM: **Coq make failing on Omega – stackoverflow.com**

**Lepticed** posted a new question on May 19, 2022 at 09:54AM: **Add an assertion and its negation to Coq – stackoverflow.com**

**Molossus Spondee** posted a new question on May 18, 2022 at 06:31PM: **Concrete inductive construction of a W-topos with Setoids in Coq – proofassistants.stackexchange.com**

**Herbal Tea** posted a new question on May 20, 2022 at 12:04AM: **How to evaluate square of a binom in coq? – stackoverflow.com**

**147pm** posted a new question on May 20, 2022 at 05:23AM: **The reference info was not found in the current environment – stackoverflow.com**

**Vladimir Prigodsky** posted a new question on May 17, 2022 at 07:47PM: **Recursive notations with forall quantifier – proofassistants.stackexchange.com**

**Herbal Tea** posted a new question on May 20, 2022 at 01:15PM: **is coq match statement exhaustive? – stackoverflow.com**

**Cahir7** posted a new question on May 20, 2022 at 01:28PM: **Running prover in why3 ,using coq - error – stackoverflow.com**

**monique** posted a new question on May 21, 2022 at 04:08AM: **How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)? – stackoverflow.com**

**Александр Степанов** posted a new question on May 23, 2022 at 03:29PM: **It is necessary to solve the problem of formal verification in "Coq" – stackoverflow.com**

**OrenIshShalom** posted a new question on May 24, 2022 at 05:43AM: **User defined language in pandoc code-block – stackoverflow.com**

**Kyle Stemen** posted a new question on May 24, 2022 at 11:29PM: **Can a Prop show that all entries of a list equal Type@{U} for any U? – proofassistants.stackexchange.com**

**Joachim Breitner** posted a new question on May 25, 2022 at 12:00PM: **Formal description of Coq’s termination checker – proofassistants.stackexchange.com**

**FH35** posted a new question on May 25, 2022 at 06:05PM: **Can't find a way to 'reverse' a constructor – stackoverflow.com**

**Александр Степанов** posted a new question on May 26, 2022 at 11:56AM: **Coq. Not sure how to write the solution in Coq – stackoverflow.com**

**Michele De Pascalis** posted a new question on May 26, 2022 at 11:38PM: **Unfolding terms created with assert in Coq – stackoverflow.com**

**Lepticed** posted a new question on May 29, 2022 at 10:15AM: **Using the transitivity of equivalence to rewrite a goal – stackoverflow.com**

**Kiran Gopinathan** posted a new question on May 30, 2022 at 10:53AM: **How to evaluate proof terms through opaque definitions? – proofassistants.stackexchange.com**

**FH35** posted a new question on May 31, 2022 at 06:25PM: **Can I prove a lemma without an additional inductive type – stackoverflow.com**

**zacque** posted a new question on June 01, 2022 at 09:15AM: **Why is my recursive definition of list_min ill-formed? – proofassistants.stackexchange.com**

**zacque** posted a new question on June 01, 2022 at 10:23AM: **Why does my previously defined function expands/computes to itself? – proofassistants.stackexchange.com**

**Lepticed** posted a new question on June 01, 2022 at 11:59AM: **Assume the negation of the goal in Coq – stackoverflow.com**

**Molossus Spondee** posted a new question on June 02, 2022 at 11:41PM: **Axiomization of Peano arithmetic in constructive first-order logic – proofassistants.stackexchange.com**

**Mathieu Borderé** posted a new question on June 09, 2022 at 09:26PM: **Coq - Assign expression to variable – stackoverflow.com**

**Molossus Spondee** posted a new question on June 09, 2022 at 11:43PM: **Why do record based inductive types with primitive projections lack an eta law? – proofassistants.stackexchange.com**

**Roland Coeurjoly** posted a new question on June 10, 2022 at 12:30AM: **How to fold simplified goal? – proofassistants.stackexchange.com**

**Roland Coeurjoly** posted a new question on June 10, 2022 at 02:24PM: **Obligation Tactic := intros. results in the Program Fixpoint with measure not being defined – proofassistants.stackexchange.com**

**Alex Nelson** posted a new question on June 11, 2022 at 12:55AM: **Coq inductive type with vector parameter lacks sufficient inductive principle – proofassistants.stackexchange.com**

**OrenIshShalom** posted a new question on June 11, 2022 at 01:28PM: **redundant eval $(opam env) needed in Dockerfile – stackoverflow.com**

**Charlie Parker** posted a new question on June 11, 2022 at 06:46PM: **How does one import the lia tactic given that the omega tactic was reprecated in Coq? – stackoverflow.com**

**Charlie Parker** posted a new question on June 11, 2022 at 07:08PM: **What is the best practice for installing external dependencies in a Coq project? – stackoverflow.com**

**Jimmy Stone** posted a new question on June 12, 2022 at 10:17AM: **How to write theorm for strong_progress not hold? – stackoverflow.com**

**Paul Snopov** posted a new question on June 12, 2022 at 04:24PM: **Question on some set theoretic problem – proofassistants.stackexchange.com**

**Paul Snopov** posted a new question on June 12, 2022 at 04:24PM: **Equational reasoning in Coq – proofassistants.stackexchange.com**

**learner123** posted a new question on June 13, 2022 at 12:38AM: **How to define a counting function with fold in Coq? – stackoverflow.com**

**learner123** posted a new question on June 13, 2022 at 02:10AM: **How to prove that in Coq that [split] and [combine] are inverses? – stackoverflow.com**

**newcoquser** posted a new question on June 13, 2022 at 02:17AM: **Problem with rewrite – proofassistants.stackexchange.com**

**learner123** posted a new question on June 13, 2022 at 02:10AM: **How to prove in Coq that [split] and [combine] are inverses? – stackoverflow.com**

**FH35** posted a new question on June 13, 2022 at 10:03AM: **Is this Lemma true in first-order intuitionistic logic? – stackoverflow.com**

**Paul Snopov** posted a new question on June 13, 2022 at 04:08PM: **Strong induction for nat in Coq – proofassistants.stackexchange.com**

**learner123** posted a new question on June 13, 2022 at 10:27PM: **How to prove that [split] and [combine] are inverses in Coq? – proofassistants.stackexchange.com**

**learner123** posted a new question on June 14, 2022 at 01:05PM: **How to prove in Coq these 2 theorems with [count_fold]? – proofassistants.stackexchange.com**

**Bolton Bailey** posted a new question on June 14, 2022 at 06:31PM: **Equivalent of range in Coq – proofassistants.stackexchange.com**

**Lepticed** posted a new question on June 15, 2022 at 07:37PM: **How to improve this proof? – stackoverflow.com**

**learner123** posted a new question on June 14, 2022 at 01:05PM: **How to prove these 2 theorems with the help of the function below? – proofassistants.stackexchange.com**

**dvr** posted a new question on June 21, 2022 at 04:52AM: **Case analysis on max - ssreflect – stackoverflow.com**

**Huan Sun** posted a new question on June 22, 2022 at 05:14AM: **How to append all list or union all set in a map's image in Isabelle – stackoverflow.com**

**dvr** posted a new question on June 22, 2022 at 11:27PM: **Coq - prove that there exists a maximal element in a non empty sequence – stackoverflow.com**

**Daigo** posted a new question on June 23, 2022 at 01:11PM: **How to prove that addition is commutative for conatural numbers in Coq – proofassistants.stackexchange.com**

**Andrey** posted a new question on June 26, 2022 at 06:02PM: **dependent pattern matching – proofassistants.stackexchange.com**

**Emma Hudson** posted a new question on June 27, 2022 at 06:15AM: **Why not have Prop : Set in Coq? – proofassistants.stackexchange.com**

**dvr** posted a new question on June 27, 2022 at 07:52PM: **Coq - proving the value of the last element in a sequence – stackoverflow.com**

**Andrey** posted a new question on June 28, 2022 at 04:19AM: **dependent pattern matching 2 – proofassistants.stackexchange.com**

**Andrey** posted a new question on June 28, 2022 at 04:19AM: **dependent pattern matching and kind of inversion – proofassistants.stackexchange.com**

**op325** posted a new question on June 29, 2022 at 11:20PM: **Prove that 1 > 1/2 in Coq – stackoverflow.com**

**op325** posted a new question on June 30, 2022 at 07:45AM: **Evaluate constant inequation in Coq – stackoverflow.com**

**Nuclear Catapult** posted a new question on July 02, 2022 at 12:39AM: **Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53) – stackoverflow.com**

**Jimmy Stone** posted a new question on July 02, 2022 at 04:12AM: **How can I write a nat in the form of term? – stackoverflow.com**

**user566206** posted a new question on July 02, 2022 at 11:34PM: **Stuck at the MApp case in Logical Foundation's pumping lemma – stackoverflow.com**

**Lepticed** posted a new question on July 03, 2022 at 12:02PM: **Best way to make a relation associative in Coq – stackoverflow.com**

**nobody** posted a new question on July 03, 2022 at 07:31PM: **Working with non-empty lists: any obviously preferrable approach? – proofassistants.stackexchange.com**

**Naitik Mundra** posted a new question on July 03, 2022 at 08:30PM: **Making sure that the function I am using returns the correct kind of values in haskell. (i.e does not contain an error "" or similar) – stackoverflow.com**

**Andrey** posted a new question on July 04, 2022 at 03:23AM: **a bit complicated dependent pattern matching where I'm not able to apply convoy – proofassistants.stackexchange.com**

**nobody** posted a new question on July 03, 2022 at 07:31PM: **Why use records for non-empty lists rather than inductively defined non-empty lists? – proofassistants.stackexchange.com**

**Andrey** posted a new question on July 04, 2022 at 03:23AM: **How to convince Coq this dependent pattern match is exhaustive? – proofassistants.stackexchange.com**

**niha kee** posted a new question on July 05, 2022 at 08:23AM: **MAXIMUM VALUE OF THE LIST – stackoverflow.com**

**Jacob woolcutt** posted a new question on July 07, 2022 at 04:26AM: **Where is the discriminate tactic defined in Coq? – proofassistants.stackexchange.com**

**user566206** posted a new question on July 07, 2022 at 09:58PM: **Cannot focus on a remaining unfocused goal in Coq – stackoverflow.com**

why wasn't this one posted here? https://proofassistants.meta.stackexchange.com/questions/214/engineerings-questions-on-internal-details-of-proof-assistant-implementations-u

the bot listens to the regular proofassistants StackExchange, and also regular StackOverflow and TCS overflow. It doesn't post meta questions.

**Charlie Parker** posted a new question on July 09, 2022 at 09:39PM: **How does one systematically traverse OCaml representations of Coq ASTs terms? – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on July 09, 2022 at 09:53PM: **How does one access the dependent type unification algorithm from Coq's internals? – stackoverflow.com**

**with-forest** posted a new question on July 10, 2022 at 03:57AM: **A Coq question : How to prove the image of the two same valued variables under a function are same? – cstheory.stackexchange.com**

**wrongbyte** posted a new question on July 10, 2022 at 06:54PM: **Understanding how pattern matching works in Coq – stackoverflow.com**

**with-forest** posted a new question on July 11, 2022 at 09:58AM: **How to Deal with Qle_bool in the progress of proving in Coq – proofassistants.stackexchange.com**

**with-forest** posted a new question on July 12, 2022 at 06:07AM: **How to prove "$x \le y$" or "$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq? – proofassistants.stackexchange.com**

seems bot doesn't put when bounties are made? here is mine: https://stackoverflow.com/questions/72924211/how-does-one-access-the-dependent-type-unification-algorithm-from-coqs-internal

Indeed, the bot is very limited: it just forwards the RSS feed (so only new questions are noticed).

**BallBoy** posted a new question on July 13, 2022 at 06:25PM: **Basics of real numbers in mathcomp (Coq) – proofassistants.stackexchange.com**

**limitedeternity** posted a new question on July 14, 2022 at 08:03PM: **Proving enumerate(...) to range(len(...)) equality – stackoverflow.com**

**Charlie Parker** posted a new question on July 14, 2022 at 09:19PM: **What are Generic Arguments in Coq and how are they structured in their OCaml code? – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on July 14, 2022 at 11:06PM: **What does it mean to have no constructors in OCaml and define a type? – stackoverflow.com**

**Charlie Parker** posted a new question on July 16, 2022 at 01:16AM: **Why does TacArg accepts a value of CAst.t type when it should only accept values of types? – proofassistants.stackexchange.com**

**Jimmy Stone** posted a new question on July 17, 2022 at 07:20AM: **Encoding records in Coq – stackoverflow.com**

**Zazaeil** posted a new question on July 18, 2022 at 09:13AM: `nat -> nat`

uncountability proved in Coq – codereview.stackexchange.com

**FH35** posted a new question on July 18, 2022 at 09:37AM: **Stuck on the proof of a simple Lemma: which induction should I use? – stackoverflow.com**

**Leo G.** posted a new question on July 18, 2022 at 07:59PM: **Coq: Implementation of splitstring and proof that nothing gets deleted – stackoverflow.com**

**Peter LeFanu Lumsdaine** posted a new question on July 19, 2022 at 02:50PM: **In VSCoq, how to issue an arbitrary Gallina query via the prompt? – proofassistants.stackexchange.com**

**niha kee** posted a new question on July 21, 2022 at 09:13AM: **Holding greater or equal relation between two terms – stackoverflow.com**

**wrongbyte** posted a new question on July 22, 2022 at 10:50PM: **Why S n' =? S n' simplifies to n' =? n' in Coq? – stackoverflow.com**

**Ana Borges** posted a new question on July 23, 2022 at 01:04PM: **Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug? – proofassistants.stackexchange.com**

**user251130** posted a new question on July 23, 2022 at 02:31PM: **Decide equality with some predicate – stackoverflow.com**

**Kyle Stemen** posted a new question on July 24, 2022 at 04:41AM: **Is coercion to a higher universe injective? – proofassistants.stackexchange.com**

**quidproquo** posted a new question on July 26, 2022 at 11:45PM: **Learning Math Proof via Proof Assistants – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on July 27, 2022 at 10:35PM: **How does one compute/create a concrete/actual string in coq to pass to functions or store in a variable/identifier? – stackoverflow.com**

**pjm** posted a new question on July 28, 2022 at 05:06PM: **Coq: rewriting under a pointwise_relation – stackoverflow.com**

**Leo G.** posted a new question on July 28, 2022 at 06:57PM: **Coq: Simpl in match pattern when having an inequality hypothesis – stackoverflow.com**

**Naqib Zahid** posted a new question on July 29, 2022 at 05:42AM: **I have been stuck on MApp for pumping lemma – stackoverflow.com**

**with-forest** posted a new question on August 02, 2022 at 09:38AM: **Define a function using another function – proofassistants.stackexchange.com**

**钱一程** posted a new question on August 02, 2022 at 11:40AM: **Unexpected coercion in constant definition – proofassistants.stackexchange.com**

**钱一程** posted a new question on August 02, 2022 at 11:40AM: **Unexpected eta expansion in constant definition – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 03, 2022 at 05:27AM: **A problem similar to intermediate value problem – proofassistants.stackexchange.com**

**Lepticed** posted a new question on August 04, 2022 at 09:42AM: **How to use a definition in Coq? – stackoverflow.com**

**Indprinciple** posted a new question on August 04, 2022 at 11:21AM: **How to instantiate non-dependent implicit arguments in Coq? – proofassistants.stackexchange.com**

**Indprinciple** posted a new question on August 04, 2022 at 11:21AM: **Non-dependent implicit argument instantiation in Coq's reference manual does not work – proofassistants.stackexchange.com**

**Malcolm Sharpe** posted a new question on August 08, 2022 at 12:39AM: **Coq: can tauto be used to prove classical tautologies? – proofassistants.stackexchange.com**

**scubed** posted a new question on August 08, 2022 at 02:10AM: **Prove equality with eq_rect without UIP – stackoverflow.com**

**with-forest** posted a new question on August 08, 2022 at 01:30PM: **Is there a method to make a hypothesis from applying two hypothesis? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 08, 2022 at 01:30PM: **Is there a tactic in Coq to make a hypothesis from applying two hypotheses? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 10, 2022 at 04:03AM: **When I destruct record, can I make a hypothesis name without 0? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 10, 2022 at 07:09AM: **Can I prove this axiom without using excluded-middle property? – proofassistants.stackexchange.com**

**Hao Yang** posted a new question on August 11, 2022 at 11:03AM: **Get stuck at the MStarApp case of Software Fundation's pumping Lemma – stackoverflow.com**

**with-forest** posted a new question on August 17, 2022 at 08:31AM: **How to define two mutually recursive functions in Coq? – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on August 20, 2022 at 03:23PM: **How does one automatically make a COQ_PROJ.opam install script automatically from a Coq Project? – stackoverflow.com**

**ax_fer** posted a new question on August 21, 2022 at 09:58PM: **Coq : replace hypothesis into implication – stackoverflow.com**

**with-forest** posted a new question on August 22, 2022 at 03:54AM: **What is the remaining goals on the shelf? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 24, 2022 at 08:07AM: **How to search only all of lemmas in a different module (in Coq)? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 24, 2022 at 08:07AM: **How can I search only all of the lemmas in a different module (in Coq)? – proofassistants.stackexchange.com**

**Netchaiev** posted a new question on August 27, 2022 at 03:34PM: **Natural deduction with coq assistant prover – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on August 30, 2022 at 02:04AM: **How do I prove this property in Coq? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 30, 2022 at 05:27AM: **How can I use a (three terms) decidable axiom in a case analysis? – proofassistants.stackexchange.com**

**with-forest** posted a new question on August 31, 2022 at 07:59AM: **How can I correspond a hypothesis to a decidable axiom in match (in Coq)? – proofassistants.stackexchange.com**

**Andrey** posted a new question on August 31, 2022 at 04:07PM: **I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working – stackoverflow.com**

**with-forest** posted a new question on September 01, 2022 at 06:35AM: **Can I unfold not all things but only one thing in Coq? – proofassistants.stackexchange.com**

**with-forest** posted a new question on September 02, 2022 at 04:12AM: **If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq? – proofassistants.stackexchange.com**

**op325** posted a new question on September 02, 2022 at 05:59PM: **setoid_rewrite failed with MathClasses Coq – stackoverflow.com**

**Bodo** posted a new question on September 08, 2022 at 02:18PM: **Overloading operators in Coq via typeclasses and notation scopes: Is there anything special about the '+' and '*' symbols? – stackoverflow.com**

**nicolas** posted a new question on September 11, 2022 at 12:09PM: **Using proof assistants to generate fast code – proofassistants.stackexchange.com**

**Rincewind** posted a new question on September 15, 2022 at 05:23PM: **.CoqMakefile.d required by CoqMakefile but not generated – proofassistants.stackexchange.com**

**Taimoor Zaeem** posted a new question on September 18, 2022 at 03:34PM: **How do I exit coqtop REPL? – stackoverflow.com**

**silver-ymz** posted a new question on September 19, 2022 at 09:17AM: **Can someone help me with this proof about the pumping lemma using coq? – stackoverflow.com**

**sudgy** posted a new question on September 28, 2022 at 12:35AM: **Coq Typeclass on Functions Gets Confused by Equality – proofassistants.stackexchange.com**

**rsaill** posted a new question on September 28, 2022 at 10:54AM: **Using VST with GCC – stackoverflow.com**

**Yu-Fang Chen** posted a new question on September 29, 2022 at 06:05AM: **Install why3-coq on MacBook Pro – stackoverflow.com**

**bruhhbruh** posted a new question on October 04, 2022 at 07:39PM: **How to convince coq that if (a * c) = (b * c), and c is not equal to 0, then a=b – stackoverflow.com**

**KingsAlpaca** posted a new question on October 05, 2022 at 03:36PM: **How to rearrange newly defined associative terms in Coq? – stackoverflow.com**

**Zak Kent** posted a new question on October 13, 2022 at 03:03AM: **Default Implementation of Coq typeclass methods – stackoverflow.com**

**Stefan ** posted a new question on October 14, 2022 at 06:32PM: **Proof of "less than or equal" transitive law in Coq – stackoverflow.com**

**Huan Sun** posted a new question on October 15, 2022 at 03:53AM: **concurrent separation logic in Isabelle – stackoverflow.com**

**Stefan ** posted a new question on October 15, 2022 at 12:20PM: **Proof that "if m <= n then max(m, n) = n" in Coq – stackoverflow.com**

**sp1ff** posted a new question on October 19, 2022 at 04:19PM: **How to scope Search to the current module only – stackoverflow.com**

**mateus filipe** posted a new question on October 19, 2022 at 11:10PM: **prove DeMorgan law in coq – stackoverflow.com**

**Dave** posted a new question on October 20, 2022 at 10:37AM: **Universe polymorphism and modules in Coq – proofassistants.stackexchange.com**

**TonyBlabla** posted a new question on October 20, 2022 at 08:06PM: **Prove that if a <= b, then max ( a , b ) = b in Coq – stackoverflow.com**

**Alessandro D'angelo** posted a new question on October 26, 2022 at 09:37PM: **Proving theorem in Coq, the number of occurances in a list is <= the lenght of this list – stackoverflow.com**

**Alessandro D'angelo** posted a new question on October 27, 2022 at 01:04AM: **Prove that the number of occurences of x in a list that has n position with valor x = n – stackoverflow.com**

**Bennett Kahn** posted a new question on November 03, 2022 at 04:54AM: **How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion? – proofassistants.stackexchange.com**

**임기정** posted a new question on November 04, 2022 at 03:16PM: **To prove the unfolding lemma for some – stackoverflow.com**

**Kamyar Mirzavaziri** posted a new question on November 05, 2022 at 06:31PM: **Definition by minimization in Coq – stackoverflow.com**

**op325** posted a new question on November 08, 2022 at 01:04PM: **Coq ssreflect - rewrite inside \big – proofassistants.stackexchange.com**

**dganti** posted a new question on November 09, 2022 at 02:02AM: **COQ returns cannot guess decreasing argument of fix. How to fix my function? – stackoverflow.com**

A message was moved from this topic to #VsCoq devs & users > VsCoq error by Karl Palmskog.

**acid** posted a new question on November 10, 2022 at 08:45AM: **How can I write a proof to match inductive type without using forall in its subterm? – stackoverflow.com**

**Charlie Parker** posted a new question on November 11, 2022 at 06:30AM: **How does one translate Lean to Coq (and visa versa)? – proofassistants.stackexchange.com**

**Nathan** posted a new question on November 16, 2022 at 04:08AM: **Why are these two proofs so different? – proofassistants.stackexchange.com**

**Åsmund Kløvstad** posted a new question on November 17, 2022 at 10:08AM: **Applying custom tactic in hypothesis – proofassistants.stackexchange.com**

**ZhangLiao** posted a new question on November 19, 2022 at 10:15AM: **Pirnting Coq definition without loading library – stackoverflow.com**

**ZhangLiao** posted a new question on November 19, 2022 at 10:15AM: **Printing Coq definition without loading library – stackoverflow.com**

**Moti** posted a new question on November 20, 2022 at 01:58PM: **Cannot open pixbuf loader module file in Windows – proofassistants.stackexchange.com**

**ch271828n** posted a new question on November 20, 2022 at 02:13PM: **Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic? – stackoverflow.com**

**Bromind** posted a new question on November 24, 2022 at 12:17AM: **Proving Union of Ensemble is not Empty_set – stackoverflow.com**

**TonyBlabla** posted a new question on November 24, 2022 at 08:29PM: **Big Step Substraction – stackoverflow.com**

**user20531868** posted a new question on November 25, 2022 at 07:02AM: **Question about failure to match wildcard character "_" – stackoverflow.com**

**ax_fer** posted a new question on November 25, 2022 at 04:04PM: **Verified software toolchain : which tactic to apply commutativity in mpred – stackoverflow.com**

**Huan Sun** posted a new question on November 29, 2022 at 05:19AM: **type variable in datatype definition – stackoverflow.com**

**xmepl** posted a new question on December 06, 2022 at 12:00PM: **Coq Problem where i dont know how to continue – stackoverflow.com**

**user1901** posted a new question on December 07, 2022 at 08:43AM: **How do I prove a record related lemma? – proofassistants.stackexchange.com**

**Charlie Parker** posted a new question on December 10, 2022 at 09:56PM: **How does one install a opam coq package that has been successfully install previously? – stackoverflow.com**

**Charlie Parker** posted a new question on December 10, 2022 at 11:53PM: **How to install the coq 8.14 package with opam pin when it says it can't find it? – stackoverflow.com**

**Charlie Parker** posted a new question on December 10, 2022 at 11:53PM: **How to install the coq 8.14 (or 8.15) package with opam pin when it says it can't find it? – stackoverflow.com**

**Charlie Parker** posted a new question on December 12, 2022 at 12:36AM: **How does one print proof terms as de bruijn indices instead of random named variables in Coq? – stackoverflow.com**

**pjm** posted a new question on December 12, 2022 at 11:24AM: **Coq: Unification fails with record – stackoverflow.com**

**Huan Sun** posted a new question on December 13, 2022 at 02:00PM: **What does InjL and InjR operator means in coq-Iris? – stackoverflow.com**

**Joshua Meyers** posted a new question on December 18, 2022 at 03:04AM: **How can I hide all proof terms? – stackoverflow.com**

**limitedeternity** posted a new question on December 18, 2022 at 07:48PM: **Proving theorems containing bitwise operators – stackoverflow.com**

**Arnie2C_A** posted a new question on December 20, 2022 at 12:35AM: **How to avoid "Cannot guess decreasing argument of fix." in Coq – stackoverflow.com**

**Jesper** posted a new question on December 21, 2022 at 03:51PM: **What was the first proof assistant with eta equality for records? – proofassistants.stackexchange.com**

**Arnie2C_A** posted a new question on December 23, 2022 at 04:06PM: **Two Coq Problems SOS: one is about IndProp, another has something to do with recursion, I guess – stackoverflow.com**

**コンピューターバカ** posted a new question on December 24, 2022 at 09:15AM: **induction integer record in coq – stackoverflow.com**

**scubed** posted a new question on December 25, 2022 at 06:42AM: **Rewrite with variable from inner scope? – stackoverflow.com**

**scubed** posted a new question on December 25, 2022 at 06:43AM: **Fix vs. Fix_sub – stackoverflow.com**

**Charles Averill** posted a new question on December 25, 2022 at 07:42PM: **How do I approach the final inductive step in plus_leb_compat_l from Software Foundations? – proofassistants.stackexchange.com**

**Charles Averill** posted a new question on December 31, 2022 at 04:51AM: **How do I approach the final step in proving the cancellation law in Coq? – proofassistants.stackexchange.com**

**Charles Averill** posted a new question on January 01, 2023 at 08:34PM: **Do you need to pass in template types to functions that accept template objects in Coq? – stackoverflow.com**

**scubed** posted a new question on January 04, 2023 at 07:45AM: **Is it possible to destruct and rewrite simultaneously? – stackoverflow.com**

**Travis Allison** posted a new question on January 06, 2023 at 04:12AM: **Exhaustiveness matching in proof objects for induction in Coq – stackoverflow.com**

**Ícaro Lorran** posted a new question on January 07, 2023 at 04:55PM: **How do I write a summation on Coq? – cstheory.stackexchange.com**

**Pietro Braione** posted a new question on January 07, 2023 at 07:37PM: **How do I define a function in Coq with if...then..else behavior? – proofassistants.stackexchange.com**

**Ben Little** posted a new question on January 07, 2023 at 10:39PM: **How to convert hypothesis with "if then else" equality into its consequent using coq? – proofassistants.stackexchange.com**

**Ícaro Lorran** posted a new question on January 08, 2023 at 05:13PM: **How to write a summation in Coq – proofassistants.stackexchange.com**

**hilberts_drinking_problem** posted a new question on January 13, 2023 at 03:27AM: **Subsequences in Coq – proofassistants.stackexchange.com**

**Ben Little** posted a new question on January 14, 2023 at 10:50PM: **Are there any ergonomic ways to deal with finite types in Coq? – proofassistants.stackexchange.com**

**amit9oct** posted a new question on January 19, 2023 at 10:55PM: **Imports in multi-file Coq projects – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on January 20, 2023 at 11:20PM: **Coq simpl failing to do beta reduction in this double fixpoint expression – proofassistants.stackexchange.com**

**Andre** posted a new question on January 21, 2023 at 04:24AM: **Vacuously true implications in Coq – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on January 20, 2023 at 11:20PM: **Coq simpl failing to do beta reduction in this fixpoint expression – proofassistants.stackexchange.com**

**dvr** posted a new question on January 23, 2023 at 07:19PM: **using addf_div for rat_numDomainType – stackoverflow.com**

**dvr** posted a new question on January 23, 2023 at 11:13PM: **Understanding \is a unit in ssreflect – stackoverflow.com**

**markasoftware** posted a new question on January 24, 2023 at 09:16PM: **In Coq, why is nat a Type, even though it's actually a Set? – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on January 24, 2023 at 10:41PM: **In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it? – proofassistants.stackexchange.com**

**user2506946** posted a new question on January 26, 2023 at 01:42AM: **Beta expansion in coq: can I make a term into a function, abstracting over another given term? – stackoverflow.com**

**FH35** posted a new question on January 28, 2023 at 05:29PM: **Is it possible to make Coq accept a class of Fixpoint functions if we provide proofs of argument size reduction? – stackoverflow.com**

**nobody** posted a new question on January 28, 2023 at 11:34PM: **Forcing evaluation of terms before extraction, or other ways to test extracted functions? – stackoverflow.com**

**Lomega** posted a new question on January 29, 2023 at 09:20PM: **"Cannot instantiate metavariable P of type ..." when destructing in Coq proof mode – stackoverflow.com**

**Adrian L** posted a new question on January 30, 2023 at 10:08PM: **Destruction of bound dependent types – proofassistants.stackexchange.com**

**Arjun Viswanathan** posted a new question on January 31, 2023 at 09:18PM: **Is there a way to redirect Coqide messages and errors to the same output? – stackoverflow.com**

**Pietro Braione** posted a new question on February 01, 2023 at 09:19PM: **What is the idiomatic way in Coq to write recursive functions over product types? – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on February 02, 2023 at 04:27PM: **How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument? – proofassistants.stackexchange.com**

**FH35** posted a new question on February 03, 2023 at 09:16AM: **Another question about how to make Coq accept a Fixpoint definition – stackoverflow.com**

**greg.** posted a new question on February 07, 2023 at 07:20AM: **Lean4: Proving that (xs = ys) = (reverse xs = reverse ys) – stackoverflow.com**

**footnotes** posted a new question on February 08, 2023 at 10:23AM: **How to prove A \/ False -> A in Coq? – stackoverflow.com**

**larsr** posted a new question on February 08, 2023 at 06:38PM: **How does one expand a fix function just one step? – stackoverflow.com**

**matteo_c** posted a new question on February 10, 2023 at 06:56PM: **Stream of all finite prefixes of a stream – proofassistants.stackexchange.com**

**sdpoll** posted a new question on February 11, 2023 at 03:47AM: **Why can't I write a function that doesn't take a type argument besides Set, Prop, or Type? – proofassistants.stackexchange.com**

**Bruno** posted a new question on February 10, 2023 at 11:07AM: **Why does Ltac not match the clause? – stackoverflow.com**

**matteo_c** posted a new question on February 13, 2023 at 06:23PM: **Two-step induction of inductive predicate on Streams – proofassistants.stackexchange.com**

**Zazaeil** posted a new question on February 13, 2023 at 10:39PM: **Does ∃! x, ∃! y, P (x, y) imply ∃! xy, P (fst xy) (snd xy)? – stackoverflow.com**

**Charlie Parker** posted a new question on February 13, 2023 at 11:51PM: **How does one make sure that coq project installed correctly when it doesn't seem to appear on opam list? – stackoverflow.com**

**Charlie Parker** posted a new question on February 14, 2023 at 07:42PM: **How do I install ocamlfind first properly before other opam packages without root permissions? – stackoverflow.com**

**Charlie Parker** posted a new question on February 14, 2023 at 08:22PM: **How does one pin/freeze a version of the dependencies of an opam project/package and then install the project with such specified dependencies? – stackoverflow.com**

**Charlie Parker** posted a new question on February 15, 2023 at 08:32PM: **How does one install coq-serapi for coq 8.10 using opam pin and ideally using a commit from coq-serapi? – stackoverflow.com**

**Charlie Parker** posted a new question on February 15, 2023 at 09:49PM: **What is the tag for menhir for coq 8.12 when installing it with opam install -y? – stackoverflow.com**

**massive coq** posted a new question on February 15, 2023 at 11:49PM: **Coq abilities and usage – proofassistants.stackexchange.com**

**M B** posted a new question on February 16, 2023 at 03:16PM: **How to get rid of opaque proof-terms in computation – proofassistants.stackexchange.com**

**Lomega** posted a new question on February 17, 2023 at 06:22PM: **Fail to destruct due to ill-typedness and even cannot give an exact term in Coq – stackoverflow.com**

**user2506946** posted a new question on February 17, 2023 at 09:58PM: **How to overload the "+" notation in Coq? – stackoverflow.com**

**David Monniaux** posted a new question on February 22, 2023 at 11:29PM: **an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert – proofassistants.stackexchange.com**

**M B** posted a new question on February 23, 2023 at 04:34PM: **Program Fixpoint decreasing on measure produces unsolvable goal – proofassistants.stackexchange.com**

**Coqerellen** posted a new question on February 23, 2023 at 05:32PM: **Destructing transitivity hypothesis on simple predicate logic – proofassistants.stackexchange.com**

**markasoftware** posted a new question on March 05, 2023 at 12:10AM: **How to break up an implication into two subgoals in Coq? – stackoverflow.com**

**asha soroushpoor** posted a new question on March 07, 2023 at 03:39PM: **Coq Induction on Hypothesis destroys the Hypothesis – proofassistants.stackexchange.com**

**Zazaeil** posted a new question on March 10, 2023 at 07:02PM: **Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself? – cstheory.stackexchange.com**

**user65526** posted a new question on March 11, 2023 at 10:45AM: **Understanding a message on CoqIde – stackoverflow.com**

**user65526** posted a new question on March 11, 2023 at 01:22PM: **Complete Atomic Boolean algebras in Coq – stackoverflow.com**

**user65526** posted a new question on March 11, 2023 at 02:53PM: **Activating nested proof – stackoverflow.com**

**user65526** posted a new question on March 11, 2023 at 05:49PM: **Definite description operator in Coq – stackoverflow.com**

**8bc3 457f** posted a new question on March 14, 2023 at 09:35AM: **How to abstract over function arity in Lean and Coq? – proofassistants.stackexchange.com**

**user65526** posted a new question on March 14, 2023 at 11:42AM: **Unclear error message regarding format and notation – stackoverflow.com**

**anonymous12345677654** posted a new question on March 14, 2023 at 04:45PM: **How can I write a filter function for sequences represented as functions in Coq? – stackoverflow.com**

**radrow** posted a new question on March 15, 2023 at 04:20PM: **How to create a custom Ltac to recursively destruct conjunctions? – stackoverflow.com**

**user65526** posted a new question on March 20, 2023 at 01:20PM: **Disjunction and the error `No product after head reduction' – stackoverflow.com**

**Felipe** posted a new question on March 20, 2023 at 06:14PM: **How to reason about equality between different datatypes? – proofassistants.stackexchange.com**

**Yousef Alhessi** posted a new question on March 20, 2023 at 09:53PM: **Proving n + S n = S (n + n) without n + S m = S (n + m) – stackoverflow.com**

**Raul Gomez** posted a new question on March 21, 2023 at 07:32AM: **I don't know how to fire up coqtail – proofassistants.stackexchange.com**

**Lepticed** posted a new question on March 21, 2023 at 09:19AM: **How to distribute an AND operator in Coq? – stackoverflow.com**

**user65526** posted a new question on March 21, 2023 at 04:39PM: **A proof by cases – stackoverflow.com**

**user65526** posted a new question on March 21, 2023 at 04:39PM: **The apply rule in proof by cases – stackoverflow.com**

**anurag** posted a new question on March 22, 2023 at 11:59AM: **How to formally verify a compiler (frontend and/or backend)? – stackoverflow.com**

**user65526** posted a new question on March 22, 2023 at 12:12PM: **Why do these theorems of propositional logic allow for the same proof in Coq? – stackoverflow.com**

**sudgy** posted a new question on March 23, 2023 at 04:24AM: **Rewrite with definitional equality and dependent types – proofassistants.stackexchange.com**

**コンピューターバカ** posted a new question on March 23, 2023 at 08:35AM: **How to use induction tactic on recursively defined functions in Coq – stackoverflow.com**

**コンピューターバカ** posted a new question on March 23, 2023 at 08:35AM: **How to proof recursively defined functions' prop in Coq – stackoverflow.com**

**anonymous12345677654** posted a new question on March 25, 2023 at 02:39PM: **What is a way to represent non-disjoint union in Coq? – stackoverflow.com**

**Mohan Radhakrishnan** posted a new question on March 25, 2023 at 06:31PM: **'coqc' does not find findlib.conf – stackoverflow.com**

**Lepticed** posted a new question on March 30, 2023 at 12:06PM: **How can I better structure Coq files? – stackoverflow.com**

**Lepticed** posted a new question on March 30, 2023 at 01:31PM: **How to deal with lemma only used once in Coq? – stackoverflow.com**

**pjm** posted a new question on March 31, 2023 at 02:54PM: **Morphism signature for dependently-typed vectors in coq – stackoverflow.com**

**Lepticed** posted a new question on April 01, 2023 at 01:32AM: **How to write the iota descriptor in Coq? – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on April 02, 2023 at 09:08PM: **Why can't I use let bindings to pattern match a 3-tuple in Coq? – proofassistants.stackexchange.com**

**Alex Byard** posted a new question on April 04, 2023 at 07:34AM: **How do different dependently typed languages compare with one another? – proofassistants.stackexchange.com**

**kbridge4096** posted a new question on April 05, 2023 at 02:09PM: **Model and Prove Unsigned Integer Operation Wrapping Behavior in Coq – proofassistants.stackexchange.com**

**Lepticed** posted a new question on April 05, 2023 at 05:09PM: **Use the contrapositive of an hypothesis in Coq – stackoverflow.com**

**Randomuser6781** posted a new question on April 12, 2023 at 03:01AM: **How do I prove this theorem with induction in COQ – proofassistants.stackexchange.com**

**anonymouse 29083** posted a new question on April 12, 2023 at 04:03AM: **Help solve these proofs – proofassistants.stackexchange.com**

**hch** posted a new question on April 12, 2023 at 09:01AM: **stuck trying to prove sublist of list – proofassistants.stackexchange.com**

**hch** posted a new question on April 12, 2023 at 09:16AM: **stuck trying to prove sublist of list – stackoverflow.com**

**HELLOBIRD 892** posted a new question on April 12, 2023 at 04:03AM: **nvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvm – proofassistants.stackexchange.com**

**anonymous12345677654** posted a new question on April 13, 2023 at 12:36PM: **Is there a library for sets that works with bool in Coq? – stackoverflow.com**

**bodacious_bandit** posted a new question on April 14, 2023 at 08:51AM: **How do I prove an expression in Coq that involves pattern matching? – proofassistants.stackexchange.com**

**Sebastian Graf** posted a new question on April 14, 2023 at 10:51AM: **Is there a formalism of "coinductive" data types with negative occurrences? – proofassistants.stackexchange.com**

**Bob** posted a new question on April 14, 2023 at 01:58PM: **How to use the pretty-printer of CompCert in the OCaml toplevel? – stackoverflow.com**

**bodacious_bandit** posted a new question on April 15, 2023 at 03:47AM: **How do I prove this property about a factorial specification in Coq? – proofassistants.stackexchange.com**

**Agnishom Chattopadhyay** posted a new question on April 17, 2023 at 02:43AM: **How to prove this correctness principle of transposition of lists of lists in Coq? – proofassistants.stackexchange.com**

**rex** posted a new question on April 17, 2023 at 05:39PM: **How to parse a string into a list of lists in Coq? – stackoverflow.com**

**randompss** posted a new question on April 18, 2023 at 05:21AM: **Trying to solve this proof using the induction theorem but I am stuck – proofassistants.stackexchange.com**

**user12456500** posted a new question on April 19, 2023 at 11:56PM: **Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]) in Coq when using inductive with integers – stackoverflow.com**

**anonymous12345677654** posted a new question on April 20, 2023 at 04:03PM: **Type coercions in finset – stackoverflow.com**

**Felipe** posted a new question on April 21, 2023 at 03:42PM: **Rewriting with heterogeneous equality (JMeq) – proofassistants.stackexchange.com**

**Pavel Shuhray** posted a new question on April 22, 2023 at 02:34AM: **Dependent sum and equality with Coq – proofassistants.stackexchange.com**

**nobody** posted a new question on April 24, 2023 at 06:58PM: `fresh`

name: use match result if variable, do something else if it's a constant – stackoverflow.com

**itsFrank** posted a new question on April 25, 2023 at 05:34AM: **How to solve this proof – proofassistants.stackexchange.com**

**itsFrank** posted a new question on April 25, 2023 at 05:34AM: **Hwo to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com**

**aaay** posted a new question on April 26, 2023 at 08:17AM: **Recursion and Pattern matching in Coq – stackoverflow.com**

**Bas Laarakker** posted a new question on April 27, 2023 at 11:15AM: **Can I show Coq equality of types without using a mapping between the types? – proofassistants.stackexchange.com**

**itsFrank** posted a new question on April 25, 2023 at 05:34AM: **How to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com**

**Qinshi Wang** posted a new question on April 28, 2023 at 03:05AM: **Coq: Unify with a pattern and get the result – proofassistants.stackexchange.com**

**8bc3 457f** posted a new question on April 30, 2023 at 08:13AM: **Inductive vs. recursive definitions – proofassistants.stackexchange.com**

**8bc3 457f** posted a new question on April 30, 2023 at 08:22AM: **Debug autorewrite in Coq – proofassistants.stackexchange.com**

**sudgy** posted a new question on May 01, 2023 at 07:05AM: **Weird use of equality in Coq – proofassistants.stackexchange.com**

**Tony Peterson** posted a new question on May 01, 2023 at 04:12PM: **Coq: Proving snd divmod doesn't depend on parameter q? – proofassistants.stackexchange.com**

**Alexandr** posted a new question on May 02, 2023 at 10:09PM: **How to proof this "Theorem spec0 : forall m n p k, (p <= k) -> (p | n) -> (p | m) -> p <= help m n k." in coq? – stackoverflow.com**

**dvr** posted a new question on May 02, 2023 at 11:22PM: **Raising a natural number, int, or rat to a rational? – stackoverflow.com**

**Felipe** posted a new question on May 03, 2023 at 01:44PM: **Reasoning about non reflexive equalities & type conversions – proofassistants.stackexchange.com**

**user21829651** posted a new question on May 05, 2023 at 10:08PM: **Software Foundations Basics Exercise - How do I access letter from grade? – stackoverflow.com**

**Jay Lee** posted a new question on May 07, 2023 at 12:10PM: **Ltac tactic that accepts an arbitrary number of quantifiers – stackoverflow.com**

**Bas Laarakker** posted a new question on May 09, 2023 at 01:07PM: **Rewriting within sigma types in Coq – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on May 10, 2023 at 06:53PM: **How to deduce this equality based on the fact that these two terms must be the same? – proofassistants.stackexchange.com**

**dvr** posted a new question on May 11, 2023 at 12:25PM: **Coerce rat to realType im math-comp/analysis – stackoverflow.com**

**Felipe Morelli** posted a new question on May 11, 2023 at 10:01PM: **Help with proofs in analysis – proofassistants.stackexchange.com**

**Henri_S** posted a new question on May 13, 2023 at 10:45AM: **Can I define nested mutually dependent types in Coq? – cstheory.stackexchange.com**

**Jack** posted a new question on May 13, 2023 at 11:42PM: **Proof List Inequality in Coq – cstheory.stackexchange.com**

**with-forest** posted a new question on May 14, 2023 at 11:03AM: **Is it possible to make a proof assistant program based on ZFC? – proofassistants.stackexchange.com**

**shooqie** posted a new question on May 15, 2023 at 02:32PM: **Non-trivial Fixpoint on nested recursive types – stackoverflow.com**

**Tilman Zuckmantel** posted a new question on May 15, 2023 at 03:34PM: **Importing a Module in Coq – stackoverflow.com**

**Jeff Witnick** posted a new question on May 15, 2023 at 08:23PM: **Induction COQ Question – proofassistants.stackexchange.com**

**Jeff Witnick** posted a new question on May 15, 2023 at 09:34PM: **Help I am confused...Proof Assistant – proofassistants.stackexchange.com**

**Jeff Witnick** posted a new question on May 16, 2023 at 12:42AM: **Equivalence Relations COQ – proofassistants.stackexchange.com**

**Jeff Witnick** posted a new question on May 16, 2023 at 02:21AM: **Help with strong induction – proofassistants.stackexchange.com**

**Jeff Witnick** posted a new question on May 16, 2023 at 02:33PM: **Help with Divisibility and GCD – proofassistants.stackexchange.com**

**deleted_user0972** posted a new question on May 15, 2023 at 08:23PM: **inductive COQ concern – proofassistants.stackexchange.com**

**randomguest0002** posted a new question on May 16, 2023 at 08:44PM: **coq proof question – proofassistants.stackexchange.com**

**randomguest0002** posted a new question on May 16, 2023 at 08:44PM: **Organizing a Coq proof – proofassistants.stackexchange.com**

**deleted_user0972** posted a new question on May 15, 2023 at 09:34PM: **No subterm matching Hab * a – proofassistants.stackexchange.com**

**Tilman Zuckmantel** posted a new question on May 19, 2023 at 10:39PM: **How to use a constructor within its own inductive definition in Coq (circular dependencies)? – stackoverflow.com**

**Tilman Zuckmantel** posted a new question on May 20, 2023 at 01:44PM: **How to use a proof about a datatype within the same datatype definition in Coq? – stackoverflow.com**

**epelaez** posted a new question on May 20, 2023 at 09:20PM: **Replace element in Coq list – stackoverflow.com**

**D Left Adjoint to U** posted a new question on May 24, 2023 at 12:02AM: **Can Coq grab some data over HTTP and then write the data as declartions in Coq itself? – proofassistants.stackexchange.com**

**Hank Lenzi** posted a new question on May 27, 2023 at 09:07PM: **Dummett's view on L.E.M. in Elements of Intuitionistic Logic – stackoverflow.com**

**shooqie** posted a new question on May 28, 2023 at 01:25AM: **Set type Variable to a concrete type inside a definition – stackoverflow.com**

**Henri_S** posted a new question on May 29, 2023 at 05:37PM: **Is there a way for Coq to recall it already proved a property for the same element in the same proof? – stackoverflow.com**

**epelaez** posted a new question on May 30, 2023 at 09:46PM: **Implementing variable replacement in a boolean polynomial function in Coq – stackoverflow.com**

**coqbeginner** posted a new question on June 01, 2023 at 08:35PM: **Notation problem – cstheory.stackexchange.com**

**nobody** posted a new question on June 02, 2023 at 04:20PM: **Including header / footer in a file generated by extraction – stackoverflow.com**

**Charlie Parker** posted a new question on June 02, 2023 at 05:25PM: **How to parse coq statements from a coq .v file the official way? – stackoverflow.com**

**R. Bosman** posted a new question on June 02, 2023 at 05:59PM: **How to teach crush to unfold definitions? – stackoverflow.com**

**epelaez** posted a new question on June 04, 2023 at 04:48AM: **Clear hypotheses after recursive Ltac – stackoverflow.com**

**Johan Buret** posted a new question on June 05, 2023 at 10:46AM: **Proving a logic riddle in Coq : testing equivalence in an Inductive set – proofassistants.stackexchange.com**

**cosmonia** posted a new question on June 06, 2023 at 02:10AM: **Proving Transitivity of Pointwise Relations on Lists in Coq – stackoverflow.com**

**lam_gam** posted a new question on June 08, 2023 at 05:19PM: **How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq? – stackoverflow.com**

**Circuit Craft** posted a new question on June 09, 2023 at 05:37AM: **Induction scheme on two arguments for custom type in Coq – proofassistants.stackexchange.com**

**Bas Laarakker** posted a new question on June 13, 2023 at 12:16PM: **Is Prop extensionality inconsistent in Coq? – stackoverflow.com**

**Farhan** posted a new question on June 13, 2023 at 09:37PM: **How can I prove Proof Irrelevance from Propositional Extensionality in Coq? – stackoverflow.com**

**Bruno** posted a new question on June 14, 2023 at 11:35AM: **Obligation generated by Equations is too strong – proofassistants.stackexchange.com**

**Moti** posted a new question on June 14, 2023 at 08:56PM: **Natural deduction in Coq – proofassistants.stackexchange.com**

**user4614475** posted a new question on June 16, 2023 at 01:56AM: **Ergonomic way to define elements of dependent records in proof mode? – stackoverflow.com**

**dvr** posted a new question on June 18, 2023 at 03:57AM: **Domain of a map in Coq – stackoverflow.com**

**Joey Eremondi** posted a new question on June 22, 2023 at 05:01PM: **Reasoning about CwFs in a proof assistant – proofassistants.stackexchange.com**

**hmltn** posted a new question on June 23, 2023 at 03:35PM: **What is the definition of Turing-complete in Coq? – proofassistants.stackexchange.com**

**7449yyc** posted a new question on June 23, 2023 at 05:57PM: **Why the Let-in construct cannot be defined as a derived form in a dependently-typed language? – stackoverflow.com**

**shooqie** posted a new question on June 23, 2023 at 11:19PM: **Tricks for proving equalities under type cast – proofassistants.stackexchange.com**

**JoJoModding** posted a new question on June 24, 2023 at 07:11PM: **Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type? – proofassistants.stackexchange.com**

**Elad Strasman** posted a new question on June 26, 2023 at 09:04PM: **coq Constructive mathematics task – stackoverflow.com**

**7449yyc** posted a new question on June 27, 2023 at 03:31AM: **What's the role of unification in Coq's core type system? – stackoverflow.com**

**radrow** posted a new question on June 27, 2023 at 07:57PM: **Is Prop a subtype of Set? – stackoverflow.com**

**yiyuan-cao** posted a new question on June 29, 2023 at 04:45PM: **Programming in Calculus of Inductive Constructions with Coq – stackoverflow.com**

**Lepticed** posted a new question on June 30, 2023 at 12:04AM: **Rewrite proposition using equivalence in Coq – stackoverflow.com**

**yiyuan-cao** posted a new question on June 29, 2023 at 04:45PM: **Programming in the Calculus of Inductive Constructions with Coq – stackoverflow.com**

**asha soroushpoor** posted a new question on July 08, 2023 at 08:21AM: **Defining 2 inductive propositions relying on each other in Coq – cs.stackexchange.com**

**shooqie** posted a new question on July 09, 2023 at 09:17PM: **Ltac - run tactic for each hypothesis of given pattern – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on July 12, 2023 at 09:14AM: **How do I debug Gallina (Coq) code? – proofassistants.stackexchange.com**

**hah** posted a new question on July 12, 2023 at 10:44AM: **Assistance with Coq: Linking Decidability of Monotonic Enumerations to a Special Principle of Omniscience – stackoverflow.com**

**matteo_c** posted a new question on July 12, 2023 at 05:17PM: **Induction error on mutually defined types in Coq – proofassistants.stackexchange.com**

**asha soroushpoor** posted a new question on July 12, 2023 at 05:47PM: **Partitioning a list with 2 elements in the middle in coq – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on July 14, 2023 at 01:01PM: **How do I extract efficient string code in Coq to OCaml? – proofassistants.stackexchange.com**

**Zara** posted a new question on July 16, 2023 at 02:01PM: **Defining Kripke models and the canonical model for $S4$ modal logic – proofassistants.stackexchange.com**

**uhbif19** posted a new question on July 16, 2023 at 04:34PM: **Formalization of matching logic (logic behind K Framework) – cstheory.stackexchange.com**

**asha soroushpoor** posted a new question on July 16, 2023 at 07:01PM: **How to prove commutation of a recursive function over a finite set defined encoded with binary nat – proofassistants.stackexchange.com**

**asha soroushpoor** posted a new question on July 16, 2023 at 07:01PM: **How to prove commutation of a recursive function over a finite set encoded with binary nat in coq – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on July 16, 2023 at 07:48PM: **What is the correct way to define a DecidableType module? – proofassistants.stackexchange.com**

**Pandemonium** posted a new question on July 17, 2023 at 05:45PM: **Unable to unify "n * 0" with "0" – stackoverflow.com**

**L--** posted a new question on July 20, 2023 at 02:55AM: **PLF: [S <: S->S] Subtyping Example Hint – stackoverflow.com**

**Lepticed** posted a new question on July 20, 2023 at 05:57PM: **Coq: A \/ A -> A – stackoverflow.com**

**toku-sa-n** posted a new question on July 21, 2023 at 03:52PM: **How to generate the AST of a Coq source code? – stackoverflow.com**

**asha soroushpoor** posted a new question on July 22, 2023 at 12:14PM: **How to define induction on arbitrary functions in coq – proofassistants.stackexchange.com**

**yiyuan-cao** posted a new question on July 25, 2023 at 11:02AM: **The significance of different types of memory models in low-level language program verification? – cstheory.stackexchange.com**

**toku-sa-n** posted a new question on July 29, 2023 at 07:27AM: **How to extract the exact information of GenArg? – stackoverflow.com**

**noCrayCray** posted a new question on July 31, 2023 at 05:59PM: **"Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think) – proofassistants.stackexchange.com**

**Julián** posted a new question on July 31, 2023 at 10:03PM: **Have Hyperdoctrines been formalized? – proofassistants.stackexchange.com**

**Agnishom Chattopadhyay** posted a new question on August 01, 2023 at 04:50AM: **Rewriting inside quantified propositions in Coq? – proofassistants.stackexchange.com**

**Jason Gross** posted a new question on August 02, 2023 at 10:08PM: **Factoring custom grammar rules for integers and lists in Coq custom entries – proofassistants.stackexchange.com**

**Lepticed** posted a new question on August 03, 2023 at 07:48PM: **Forall and exists in a Coq proof – stackoverflow.com**

**paulotorrens** posted a new question on August 08, 2023 at 05:05PM: **How to reason about and extract code for inductive types with negative occurrences in Coq? – proofassistants.stackexchange.com**

**Vladimir Prigodsky** posted a new question on August 08, 2023 at 05:14PM: **Using CoqHammer from Ltac2 – proofassistants.stackexchange.com**

**Kyle Lin** posted a new question on August 09, 2023 at 02:47AM: **Coq: Would adding "inline inductive definition expressions" introduce inconsistency? – proofassistants.stackexchange.com**

**TomR** posted a new question on August 11, 2023 at 01:01PM: **Is there formalization of (any) model of ∞-category in (any) proof assistant? And if there is none, what is the challenge of creating one? – proofassistants.stackexchange.com**

**Julián** posted a new question on August 12, 2023 at 05:30PM: **How to install dependencies correctly? [Cannot find a physical path bound to logical path] – proofassistants.stackexchange.com**

**TomR** posted a new question on August 12, 2023 at 09:18PM: **How to download (e.g. from Github) Coq, if its main site is down? – proofassistants.stackexchange.com**

**Kyle Lin** posted a new question on August 15, 2023 at 09:48AM: **Can you always replace mutually recursive references with parameters? – proofassistants.stackexchange.com**

**Kyle Lin** posted a new question on August 15, 2023 at 10:57AM: **Why does Coq not allow constructor argument types to be strictly positive mutual inductive types? – proofassistants.stackexchange.com**

**Gregory Bush** posted a new question on August 15, 2023 at 04:12PM: **Type-specific proof of UIP for type with decidable equality using induction – stackoverflow.com**

**vzhilin** posted a new question on August 16, 2023 at 02:32PM: **List without gaps in Coq – stackoverflow.com**

**Nicolas Rinaudo** posted a new question on August 16, 2023 at 10:29PM: **Force Coq to simplify unfalsifiable pattern matches – stackoverflow.com**

**userl6kgPo0ixv** posted a new question on August 17, 2023 at 01:28PM: **Proving function existence in Coq – proofassistants.stackexchange.com**

**noCrayCray** posted a new question on August 17, 2023 at 02:31PM: **İnduction/inversion and others in coq – proofassistants.stackexchange.com**

**Agnishom Chattopadhyay** posted a new question on August 17, 2023 at 08:30PM: **Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other – proofassistants.stackexchange.com**

**E030E03** posted a new question on August 19, 2023 at 11:54AM: **Coq specifying the type of a variable – proofassistants.stackexchange.com**

**joro** posted a new question on August 23, 2023 at 02:31PM: **How bad is Coq proving both $T$ and $\lnot T$? – mathoverflow.net**

**PeterTN** posted a new question on August 24, 2023 at 08:20PM: **Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt – stackoverflow.com**

**arshiamoeini** posted a new question on August 26, 2023 at 10:52PM: **formalization of partial function for counting – cs.stackexchange.com**

**arshiamoeini** posted a new question on August 27, 2023 at 04:47PM: **formalization of partial function for counting – proofassistants.stackexchange.com**

**arshiamoeini** posted a new question on August 27, 2023 at 04:47PM: **Formalization of partial functions for combinatorial counting – proofassistants.stackexchange.com**

**acogrunge** posted a new question on August 30, 2023 at 01:15AM: **false = true problem when solving Lemma in Coq – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on August 31, 2023 at 08:56PM: **Defining a Recursive Function decreasing on one argument with < and another structurally – proofassistants.stackexchange.com**

**Andrii Kozytskyi** posted a new question on September 01, 2023 at 09:08AM: **Specializing forall quantifiers in Coq – proofassistants.stackexchange.com**

**Circuit Craft** posted a new question on September 05, 2023 at 06:21PM: **Eliminating dependent destruction in Coq – proofassistants.stackexchange.com**

**noCrayCray** posted a new question on September 06, 2023 at 05:12PM: **confused about stlc from Programming Language Foundations – proofassistants.stackexchange.com**

**Maya** posted a new question on September 07, 2023 at 01:32PM: **Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example? – proofassistants.stackexchange.com**

**kunkun** posted a new question on September 10, 2023 at 07:03AM: **How to proof by natural number case analysis in Coq? – stackoverflow.com**

**user3598542** posted a new question on September 12, 2023 at 12:40AM: **How to represent 2D array in Verifiable C – stackoverflow.com**

**user1953221** posted a new question on September 12, 2023 at 08:22AM: **Understanding TLC's finite map library – stackoverflow.com**

**jschroed TV** posted a new question on September 14, 2023 at 05:57PM: **vscoq language server failed installing – stackoverflow.com**

**Weier** posted a new question on September 19, 2023 at 02:27PM: **(Dis)Advantages of basing a proof assistant on CH correspondence? – proofassistants.stackexchange.com**

**someStudentCS** posted a new question on September 19, 2023 at 06:36PM: **Coq: Cannot infer the type of function in environment – stackoverflow.com**

**someStudentCS** posted a new question on September 19, 2023 at 06:36PM: **Cannot infer the type of function in environment – stackoverflow.com**

**Sam Ni** posted a new question on September 21, 2023 at 06:45PM: **coq, is there a tartic to auto solve simle inequality such as a < b for real numbers? – stackoverflow.com**

**Sheldon** posted a new question on September 26, 2023 at 06:22AM: **iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq – proofassistants.stackexchange.com**

**Michael Hennebry** posted a new question on September 29, 2023 at 02:47AM: **gappa seems to generate bad Coq – proofassistants.stackexchange.com**

**Jon** posted a new question on October 01, 2023 at 08:00PM: **Eta-equality for records: the case of semigroups – proofassistants.stackexchange.com**

**palmskog** posted a new question on October 03, 2023 at 03:54PM: **How do I write a minimal working example (MWE) in Coq to demonstrate some problem? – proofassistants.stackexchange.com**

**Tony Peterson** posted a new question on October 05, 2023 at 09:11PM: **Proving that a minimum example exists if any example exists in nat – proofassistants.stackexchange.com**

**Adrian L** posted a new question on October 10, 2023 at 10:39PM: **Use proof irrelevance in cast – proofassistants.stackexchange.com**

**ghilesZ** posted a new question on October 12, 2023 at 01:57PM: **Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)? – stackoverflow.com**

**kunkun** posted a new question on October 16, 2023 at 06:26PM: **How to prove forall x y, x<=y -> div2 x <= div2 y in coq? – stackoverflow.com**

**Drona Nagarajan** posted a new question on October 17, 2023 at 12:04AM: **Forward leads to stack-overflow – stackoverflow.com**

**Huan Sun** posted a new question on October 18, 2023 at 07:33AM: **How to use Isabelle's command line commands in macOS – stackoverflow.com**

**Jon** posted a new question on October 19, 2023 at 10:57AM: **Universe polymorphism and Coq standard library – proofassistants.stackexchange.com**

**Drona Nagarajan** posted a new question on October 20, 2023 at 03:55PM: **How do I write a C loop as a Fixpoint in Coq? – stackoverflow.com**

**bluesquare** posted a new question on October 21, 2023 at 04:25AM: **True in Goal State Coq – stackoverflow.com**

**7Orion7** posted a new question on October 26, 2023 at 09:36PM: **Can't find Lemma for set equality in stdpp library – stackoverflow.com**

**7Orion7** posted a new question on October 27, 2023 at 11:34AM: **Custom tactics provided by libraries – stackoverflow.com**

**Abde Mojito** posted a new question on October 28, 2023 at 02:31PM: **Cannot find a physical path bound to logical path ImpCEvalFun with prefix LF – proofassistants.stackexchange.com**

**Abde Mojito** posted a new question on October 28, 2023 at 02:31PM: **Help with fixing a Coq installation using docker and vscoq – proofassistants.stackexchange.com**

**Felipe** posted a new question on October 30, 2023 at 03:27PM: **Problem working with FMapWeakList and Parametrized Records – proofassistants.stackexchange.com**

**Drona Nagarajan** posted a new question on October 31, 2023 at 09:06AM: **Unable to proceed with list induction – stackoverflow.com**

**Tempestas Ludi** posted a new question on October 31, 2023 at 02:45PM: **Continue a section (with context) in coq – proofassistants.stackexchange.com**

**Tiago Campos** posted a new question on November 01, 2023 at 05:40AM: **Why inductive types (or variants) are so rigid in terms of the set of constructors – proofassistants.stackexchange.com**

**mell_o_tron** posted a new question on November 02, 2023 at 10:42AM: **How to reason about sets in Coq? - Defining Complete Lattices – stackoverflow.com**

**Random Citizen** posted a new question on November 05, 2023 at 04:52PM: **Why is specialize not an invalid tactic within a proof? – stackoverflow.com**

**Circuit Craft** posted a new question on November 06, 2023 at 10:55PM: **Universe inconsistency errors when using ZF model in Coq – proofassistants.stackexchange.com**

**mell_o_tron** posted a new question on November 10, 2023 at 11:51AM: **Coq: Is there a way to define "map" for Ensemble – stackoverflow.com**

**kunkun** posted a new question on November 12, 2023 at 12:02PM: **How to continue case analysis of a nested match in coq? – stackoverflow.com**

**Chris Henson** posted a new question on November 16, 2023 at 05:14PM: **How to express that two equivalence relations can setoid rewrite across each other (Coq) – proofassistants.stackexchange.com**

**Andrey** posted a new question on November 17, 2023 at 12:36PM: **problem with unification – proofassistants.stackexchange.com**

**Greg Nisbet** posted a new question on November 18, 2023 at 06:46PM: **How to check a Zenon-generated proof with Coq? – proofassistants.stackexchange.com**

**Sheldon** posted a new question on November 19, 2023 at 12:15PM: **reference ospecialize and variable prim_base_irreducible not found in the current environment – proofassistants.stackexchange.com**

**asha soroushpoor** posted a new question on November 19, 2023 at 05:35PM: **What is the best way to learn Iris completely independently – proofassistants.stackexchange.com**

**Marcus** posted a new question on November 20, 2023 at 10:43PM: **Coq code in LaTeX using lstcoq does not work – stackoverflow.com**

**paulotorrens** posted a new question on November 21, 2023 at 10:50AM: **Unfolding constants while rewriting using rewrite_strat and a hint database – proofassistants.stackexchange.com**

**lindvv** posted a new question on November 22, 2023 at 05:51AM: **How to prove the goals in more elegant way using ssreflect? – stackoverflow.com**

**Marcus** posted a new question on November 23, 2023 at 08:20PM: **How to prove an inequality – stackoverflow.com**

**bluesquare** posted a new question on November 27, 2023 at 07:21PM: **How do I install a library in coq? (MacOS) – stackoverflow.com**

**luxuriant_lettuce** posted a new question on December 01, 2023 at 08:47AM: **How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq – stackoverflow.com**

**e2e4** posted a new question on December 02, 2023 at 07:50PM: **Need help to prove (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅) – stackoverflow.com**

**Link L** posted a new question on December 06, 2023 at 02:00AM: **What is the difference between these inductive definitions in Coq? – proofassistants.stackexchange.com**

**Yeshe Tenley** posted a new question on December 06, 2023 at 05:44AM: **LEM, the halting problem, the curry-howard correspondence -> deep connection? – proofassistants.stackexchange.com**

**Daniel Bee** posted a new question on December 06, 2023 at 10:36PM: **Coq makefile complains about extension points on Windows 10 – proofassistants.stackexchange.com**

**user3083** posted a new question on December 07, 2023 at 04:05AM: **Using verdi raft. How do I import it into my Coq Project? – proofassistants.stackexchange.com**

**Yeshe Tenley** posted a new question on December 07, 2023 at 03:03PM: **A CoQ program which constructively proves the halting problem – proofassistants.stackexchange.com**

**Gul** posted a new question on December 07, 2023 at 05:16PM: **plz any guide me for coq extension in VS code – proofassistants.stackexchange.com**

**Andrea Tirelli** posted a new question on December 08, 2023 at 04:47PM: **Proof of Constant folding in Coq for IMP using Interaction Trees – proofassistants.stackexchange.com**

**Link L** posted a new question on December 10, 2023 at 05:26AM: **How to to use the fact that combining these hypothesis is false in Coq – proofassistants.stackexchange.com**

**user1953221** posted a new question on December 12, 2023 at 06:52AM: **Forward simulation with partial simulation relation – proofassistants.stackexchange.com**

**someStudentCS** posted a new question on December 15, 2023 at 09:10PM: **Iris/Coq replacing literal – stackoverflow.com**

**yiyuan-cao** posted a new question on December 21, 2023 at 03:37PM: **How to reason with notations directly? – proofassistants.stackexchange.com**

**Matt** posted a new question on December 22, 2023 at 06:23PM: **How can I generate equalities from an application in Coq? – proofassistants.stackexchange.com**

**Andreas Florath** posted a new question on December 31, 2023 at 10:07AM: **Efficient Record Construction in Coq: Is Direct Proof Inclusion Possible? – stackoverflow.com**

**Rand00** posted a new question on January 05, 2024 at 08:50PM: **Coq / Lean endpoint for GPT actions – proofassistants.stackexchange.com**

**scubed** posted a new question on January 09, 2024 at 06:35AM: **Dependent equality with 2 different type functions – stackoverflow.com**

**Sajuuk** posted a new question on January 09, 2024 at 04:06PM: **How to correctly feed type argument in this toy theorem? – proofassistants.stackexchange.com**

**radrow** posted a new question on January 10, 2024 at 05:10PM: **How to define a recursive notation with overlapping production? – stackoverflow.com**

**Michael Schmidt** posted a new question on January 10, 2024 at 10:39PM: **How to apply constructor injectivity in the goal – proofassistants.stackexchange.com**

**Bruno** posted a new question on January 11, 2024 at 04:43AM: **Are there drawbacks in Coq to make implicit some arguments? – proofassistants.stackexchange.com**

**Bruno** posted a new question on January 11, 2024 at 04:43AM: **In Coq, are there drawbacks in making implicit some arguments? – proofassistants.stackexchange.com**

**Lepticed** posted a new question on January 12, 2024 at 11:03AM: **In Coq, what would be the steps to prove the correctness of a function that solves puzzles like Sudoku or Takuzu? – stackoverflow.com**

**user23220385** posted a new question on January 12, 2024 at 10:55PM: **Proving "proof methods" as theorems in type-theory based proof systems – proofassistants.stackexchange.com**

**Andreas Florath** posted a new question on January 16, 2024 at 04:44PM: **Does import not only import but also change existing definitions? – stackoverflow.com**

**noCrayCray** posted a new question on January 20, 2024 at 03:54PM: **How to import unimath for coq – proofassistants.stackexchange.com**

**lottiebegnl** posted a new question on January 22, 2024 at 01:38PM: **Help with my project in the Coq proof assistant – proofassistants.stackexchange.com**

**Natasha Klaus** posted a new question on January 22, 2024 at 01:56PM: **How to make Spoq generate high-level specifications in Coq (not just AST) for the functions in LLVM IR – stackoverflow.com**

**noCrayCray** posted a new question on January 22, 2024 at 04:23PM: **how to inductively define paths from paths using unimath – proofassistants.stackexchange.com**

**mell_o_tron** posted a new question on January 23, 2024 at 07:15PM: **Why does coq not recognize that None = Some v is false? – stackoverflow.com**

**lukmik** posted a new question on January 24, 2024 at 09:23PM: **How to prove this in CoqIDE – stackoverflow.com**

**Liu Xiaoyi** posted a new question on January 25, 2024 at 11:47AM: **Does equality in $\Sigma_{(x : X)} x = x$ implies UIP? – proofassistants.stackexchange.com**

**Lepticed** posted a new question on January 25, 2024 at 03:54PM: **Proving some theorems on the function index in Coq – stackoverflow.com**

**Henrique Guerra** posted a new question on January 25, 2024 at 07:30PM: **Coq/Ltac: is it possible to design a tactic that says the goal is proved when a decision procedure proves it, without the proof term? – stackoverflow.com**

**C.E.Sally** posted a new question on January 27, 2024 at 03:07AM: **How to get term describing case of pattern match in Coq – proofassistants.stackexchange.com**

**C.E.Sally** posted a new question on January 27, 2024 at 06:32AM: **Is there a way to rename parameters in a module type in Coq? – proofassistants.stackexchange.com**

**VikramG** posted a new question on January 29, 2024 at 10:19AM: **Software Foundations (lf): proving leb_plus_exists and plus_leb_exists – stackoverflow.com**

**C.E.Sally** posted a new question on January 27, 2024 at 06:32AM: **Is there a way to rename parameters when including/reusing a module type in Coq? – proofassistants.stackexchange.com**

**Henrique Guerra** posted a new question on January 30, 2024 at 06:40PM: **Coq/Ocaml API: matching Constr.t representing a forall never matches Constr.Prod – stackoverflow.com**

**lukmik** posted a new question on January 24, 2024 at 09:23PM: **How to prove this in Coq – stackoverflow.com**

**VikramG** posted a new question on January 31, 2024 at 12:21PM: **How do I apply (S n' <=? m) = true to S n' <= m? – stackoverflow.com**

**Lepticed** posted a new question on February 01, 2024 at 12:26PM: **Prove theorem about the last element of a list – stackoverflow.com**

**Ulises Torrella** posted a new question on February 01, 2024 at 03:58PM: **Coq : Using a parametrised Type from within a Module – stackoverflow.com**

**Ulises Torrella** posted a new question on February 01, 2024 at 03:58PM: **Coq : Using a parametrized Type from within a Module – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on February 01, 2024 at 08:12PM: **Selecting both a hypothesis and Goal while applying a tactic – proofassistants.stackexchange.com**

FTR, IFTTT has disabled the integration that was powering this feed without warning and now I would need to pay to reactivate it, so I'm going to look for alternatives, but in the meantime, this feed won't be updated.

calvin posted a new question on 2024-02-07T18:36:02Z: How can I handle this `false = true`

case? – stackoverflow.com

**calvin** posted a new question on 2024-02-07T14:30:55Z: **Why can't I destruct or discriminate here? – stackoverflow.com**

The bot is back on. FWIW, I use this RSS feed on StackExchange to follow the data: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites

I switched from IFTTT to Zapier to post new messages on this topic every time a new item appears in this feed.

There are 6 questions in this feed that were skipped in the week of downtime (since Feb 2nd).

**someStudentCS** posted a new question on 2024-02-11T17:17:05Z: **Coq inductive not right form – stackoverflow.com**

**scubed** posted a new question on 2024-02-12T02:32:16Z: **How do I move a let variable to a separate hypothesis? – stackoverflow.com**

**Patrick Nicodemus** posted a new question on 2024-02-12T15:10:54Z: **What are the principal differences between Agda's core type theory and Coq's? – proofassistants.stackexchange.com**

**catie** posted a new question on 2024-02-12T21:09:39Z: **VSCoq Error: Connection to server got closed. Server will not be restarted – stackoverflow.com**

**Johan Buret** posted a new question on 2024-02-13T22:10:58Z: **Proving that equality is decidable on an Inductive Set – proofassistants.stackexchange.com**

**Ian Maxwell** posted a new question on 2024-02-17T16:15:11Z: **Defining and using bisimilarity for negatively-defined conatural numbers – proofassistants.stackexchange.com**

**Deedit** posted a new question on 2024-02-17T23:44:38Z: **Decider for lists In Fixpoint – stackoverflow.com**

**Pablo Martín Viñuelas** posted a new question on 2024-02-18T19:33:45Z: **Unable to install Coq-Polyhedra – stackoverflow.com**

**user23439360** posted a new question on 2024-02-19T08:31:27Z: **Multiple Assignements in a Coq Map to the same value – stackoverflow.com**

**andreas** posted a new question on 2024-02-22T11:58:36Z: **The specialize tatic in Coq does not work well with typeclasses? – stackoverflow.com**

**Dave** posted a new question on 2024-02-22T18:21:42Z: **Stuck in a proof about sum types and nonempty lists – proofassistants.stackexchange.com**

**Soundwave** posted a new question on 2024-02-23T05:43:41Z: **Coq - Overloading over multiple parameters with canonical structures – proofassistants.stackexchange.com**

**LightQuantum** posted a new question on 2024-02-25T17:01:46Z: **Induction on indexed type family without JMeq – proofassistants.stackexchange.com**

**someStudentCS** posted a new question on 2024-02-25T19:12:23Z: **Coq Decreasing Argument mapping – stackoverflow.com**

**Uladzimir Treihis** posted a new question on 2024-02-27T14:45:19Z: **Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix) – proofassistants.stackexchange.com**

**Ulises Torrella** posted a new question on 2024-02-28T12:39:10Z: **Coq can't define an inductive proposition – stackoverflow.com**

**Julius H.** posted a new question on 2024-03-04T14:45:48Z: **Can proof assistants reflect the informal notion of a “theory” as the formally logical notion of a “theory”? – proofassistants.stackexchange.com**

**ayylien** posted a new question on 2024-03-12T21:33:39Z: **Split multiple conjuncts in the goal – stackoverflow.com**

**blonded04** posted a new question on 2024-03-13T00:48:52Z: **What dependent induction tactic does in Coq and how to use it – stackoverflow.com**

**Charles Averill** posted a new question on 2024-03-14T11:19:21Z: **How to prove non-existence of terms that contain themselves in Coq – proofassistants.stackexchange.com**

**Charles Averill** posted a new question on 2024-03-15T16:12:14Z: **Proving non-existence of "least" subtype generator in Coq – proofassistants.stackexchange.com**

**Snowybluesky** posted a new question on 2024-03-16T12:12:51Z: **For formal proofs of graph structures and algorithms, which proof assistant should I learn? – proofassistants.stackexchange.com**

**hugomg** posted a new question on 2024-03-18T01:42:50Z: **In Coq, what tactic can I use to remove a True precondition from a hypothesis – proofassistants.stackexchange.com**

**ayylien** posted a new question on 2024-03-19T04:22:54Z: **Understanding nat_ind2 in Logical Foundations – stackoverflow.com**

**Henrique Guerra** posted a new question on 2024-03-19T13:17:59Z: **Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq? – stackoverflow.com**

**user6584** posted a new question on 2024-03-20T14:56:32Z: **Syntax of the case tactic in coq – stackoverflow.com**

**user2628206** posted a new question on 2024-03-21T03:28:56Z: **Assistance using destruct on an equality proof for functors – proofassistants.stackexchange.com**

**user6584** posted a new question on 2024-03-21T18:52:04Z: **Showing polynomial equality in coq/ssreflect – stackoverflow.com**

**Julius Hamilton** posted a new question on 2024-03-22T22:50:18Z: **Why does the following Coq code fail to meet Coq's positivity requirement for inductive types? – proofassistants.stackexchange.com**

**mindconnect.cc** posted a new question on 2024-03-23T12:08:09Z: **How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)? – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on 2024-03-23T22:27:19Z: **Creating a tactic for 'destructing' a list by last element? – proofassistants.stackexchange.com**

**name1les** posted a new question on 2024-03-26T11:27:51Z: **Coq: Language server crashes when trying to introduce an equality-hypothesis – proofassistants.stackexchange.com**

**toku-sa-n** posted a new question on 2024-03-27T07:28:16Z: **Is there a function that returns a list of values with specific type in OCaml? – stackoverflow.com**

**Kevin Chen** posted a new question on 2024-03-27T22:06:22Z: **write a coq code to proof constant not surjective – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on 2024-03-28T19:07:48Z: **Tactic to Propify a bool expression – proofassistants.stackexchange.com**

**Natasha Klaus** posted a new question on 2024-03-29T10:48:25Z: **Coq : mutually recursive definitions with [mrec] in InteractionTrees Library – stackoverflow.com**

**Julius Hamilton** posted a new question on 2024-03-29T19:36:53Z: **Analysis of proof that for a category which is also a poset, every diagram commutes – proofassistants.stackexchange.com**

**RataMágica** posted a new question on 2024-04-02T21:04:30Z: **what symbols can I use in coq? – proofassistants.stackexchange.com**

**Hiroki Chen** posted a new question on 2024-04-05T17:03:47Z: **What is the most ergonomic way to eliminate multiple similar goals in Coq? – proofassistants.stackexchange.com**

**user2628206** posted a new question on 2024-04-06T01:44:44Z: **Packaging Mathematical Structures in Coq: Help Understanding a Definition – proofassistants.stackexchange.com**

**Patrick Nicodemus** posted a new question on 2024-04-07T00:15:52Z: **Coq - Are there functions which are provably equal but not definitionally equal? – proofassistants.stackexchange.com**

**The Circle** posted a new question on 2024-04-07T16:19:14Z: **Coq Importing Lemma from standard library module defined as Module Type ?? (Import ?? : ??) (Import ?? : ?? ??). – proofassistants.stackexchange.com**

**Pietro Braione** posted a new question on 2024-04-08T10:33:12Z: **How do I express a negative premise in Coq? – proofassistants.stackexchange.com**

**The Circle** posted a new question on 2024-04-07T16:19:14Z: **How to use a lemma that is defined in a Coq module? – proofassistants.stackexchange.com**

**udduu** posted a new question on 2024-04-13T19:21:32Z: **Is is possible to rename a coq term? – stackoverflow.com**

**The Circle** posted a new question on 2024-04-14T18:28:49Z: **Coq, Merging two forall definitions ranging over the same types – proofassistants.stackexchange.com**

**ignorant student** posted a new question on 2024-04-15T07:48:03Z: **Dealing an equality with coq. - beginner's question – proofassistants.stackexchange.com**

**Siam** posted a new question on 2024-04-16T02:21:30Z: **Proof for Question V.10 – proofassistants.stackexchange.com**

**Kevin Chen** posted a new question on 2024-04-16T19:36:58Z: **How to write a coq code for sum square, start with Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1). Proof – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on 2024-04-16T20:53:02Z: **How do I enable this kind of rewriting? – proofassistants.stackexchange.com**

**camsterwheel** posted a new question on 2024-04-17T13:45:44Z: **Trouble proving a theorem using induction – proofassistants.stackexchange.com**

**camsterwheel** posted a new question on 2024-04-17T13:45:44Z: **Trouble proving a theorem using induction in Coq – proofassistants.stackexchange.com**

**scubed** posted a new question on 2024-04-18T05:37:40Z: **Inductive from CoInductive? – stackoverflow.com**

**RudeOnion** posted a new question on 2024-04-18T17:00:42Z: **Struggling with the three_and_five theorem – proofassistants.stackexchange.com**

**scubed** posted a new question on 2024-04-19T05:55:26Z: **Inductive from CoInductive? – proofassistants.stackexchange.com**

**radrow** posted a new question on 2024-04-23T09:17:18Z: **How to instruct auto to simplify the goal during proof search? – stackoverflow.com**

**toku-sa-n** posted a new question on 2024-04-23T22:03:30Z: **Installing Coq on Windows on GitHub Actions succeeds on a repo, and fails on another repo – stackoverflow.com**

**Djoser** posted a new question on 2024-04-24T21:38:25Z: **Book on Coq that helps me write proofs regarding integral equations – proofassistants.stackexchange.com**

**Natasha Klaus** posted a new question on 2024-04-26T12:22:46Z: **InteractionTrees library - simple program on ASM – stackoverflow.com**

**Glyn Webster** posted a new question on 2024-04-26T23:00:54Z: **My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix." – proofassistants.stackexchange.com**

**io ieong** posted a new question on 2024-04-27T15:09:58Z: **How to use coq to prove this firstn and nth question? – stackoverflow.com**

**Jay Lee** posted a new question on 2024-04-28T18:10:54Z: **What does induction ... in ... do in Coq? – proofassistants.stackexchange.com**

**Doktor Diagoras** posted a new question on 2024-04-28T20:08:18Z: **Eliminating impossible branches in Coq dependent pattern matching – stackoverflow.com**

**mindconnect.cc** posted a new question on 2024-04-29T09:14:41Z: **Is there an intuitionistic proof of (A -> B \/ C) -> (A -> B) \/ (A -> C)? – stackoverflow.com**

**Agnishom Chattopadhyay** posted a new question on 2024-04-30T21:45:21Z: **Rewriting/Applying unidirectional morphisms in Coq – proofassistants.stackexchange.com**

**Glyn Webster** posted a new question on 2024-05-02T09:13:01Z: **How do I define an induction principle for a type with a nested list of tuples? – proofassistants.stackexchange.com**

**sesame ball** posted a new question on 2024-05-02T18:15:14Z: **How to prove that forall n m, n <= m -> m <= n -> n = m – stackoverflow.com**

**user2628206** posted a new question on 2024-05-04T02:20:44Z: **Ltac, How to intro a fresh variable which may already have a good estiblished name given by a universal quantifier? – proofassistants.stackexchange.com**

**Sana** posted a new question on 2024-05-06T03:37:43Z: **Error: Cannot find a physical path bound to logical path Strands. in coq – stackoverflow.com**

**return true** posted a new question on 2024-05-08T10:44:54Z: **Error Abstracting over the term leads to a term which is ill-typed when doing a destruct – proofassistants.stackexchange.com**

**Ke Du** posted a new question on 2024-05-10T09:10:20Z: **What's the idiomatic way to instantiate a tuple of evars in Ltac2? – proofassistants.stackexchange.com**

**FH35** posted a new question on 2024-05-13T08:19:58Z: **Lemma about a graph in Coq – stackoverflow.com**

**radrow** posted a new question on 2024-05-13T17:21:27Z: **How to mix sections with hints in Coq? – stackoverflow.com**

**Cs_J** posted a new question on 2024-05-15T03:33:59Z: **Defining mutually recursive types in Coq? – stackoverflow.com**

**Bruno Rafael** posted a new question on 2024-05-15T15:06:13Z: **About the use of command Canonical in Coq for mantaining Record Type information – proofassistants.stackexchange.com**

**Jennifer Paykin** posted a new question on 2024-05-15T23:04:28Z: **How do I properly interact with CertiCoq's garbage collector when calling library functions from C++? – proofassistants.stackexchange.com**

**return true** posted a new question on 2024-05-16T10:50:32Z: **Ltac with explicit constructor not working – proofassistants.stackexchange.com**

Last updated: May 18 2024 at 08:40 UTC