Stream: Coq users

Topic: New Stack Exchange question


view this post on Zulip StackExchange Bot (Jun 24 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Jun 24 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Jun 25 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Jun 26 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Jun 26 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jun 26 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jun 27 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Jun 28 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Jun 28 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Jun 28 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Jun 29 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Jun 30 2020 at 23:48):

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

view this post on Zulip StackExchange Bot (Jul 01 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Jul 01 2020 at 23:48):

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

view this post on Zulip StackExchange Bot (Jul 03 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Jul 05 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Jul 05 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 07 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 08 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Jul 09 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Jul 09 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Jul 12 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 13 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Jul 13 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 14 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 01:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Jul 15 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Jul 16 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Jul 16 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 19 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Jul 21 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Jul 22 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Jul 22 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Jul 23 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Jul 23 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Jul 25 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Jul 27 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Jul 28 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 28 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Jul 28 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Jul 29 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Jul 30 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Jul 30 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 31 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Jul 31 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Aug 01 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Aug 04 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Aug 05 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Aug 06 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Aug 07 2020 at 01:48):

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

view this post on Zulip StackExchange Bot (Aug 08 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Aug 09 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Aug 09 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Aug 09 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Aug 09 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Aug 09 2020 at 23:48):

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

view this post on Zulip StackExchange Bot (Aug 10 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Aug 12 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Aug 12 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Aug 12 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Aug 13 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Aug 14 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Aug 14 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Aug 14 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Aug 15 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Aug 15 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Aug 21 2020 at 13:52):

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

view this post on Zulip StackExchange Bot (Aug 22 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Aug 23 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Aug 24 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Aug 24 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Aug 26 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Aug 27 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Aug 28 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Aug 29 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Aug 31 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Sep 01 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Sep 01 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Sep 02 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Sep 02 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Sep 02 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Sep 03 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Sep 03 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Sep 07 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Sep 08 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Sep 08 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Sep 08 2020 at 23:48):

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

view this post on Zulip StackExchange Bot (Sep 09 2020 at 04:48):

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

view this post on Zulip StackExchange Bot (Sep 09 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Sep 10 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Sep 10 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Sep 14 2020 at 01:48):

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

view this post on Zulip StackExchange Bot (Sep 15 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Sep 15 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Sep 17 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Sep 17 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Sep 18 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Sep 19 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Sep 20 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Sep 21 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Sep 21 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Sep 21 2020 at 17:59):

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

view this post on Zulip StackExchange Bot (Sep 22 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Sep 24 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Sep 26 2020 at 04:48):

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

view this post on Zulip StackExchange Bot (Sep 26 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Sep 26 2020 at 18:48):

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

view this post on Zulip StackExchange Bot (Sep 29 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Sep 29 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Sep 30 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Oct 02 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Oct 03 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Oct 05 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Oct 05 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Oct 05 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Oct 06 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Oct 06 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Oct 06 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Oct 06 2020 at 12:51):

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

view this post on Zulip StackExchange Bot (Oct 06 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Oct 07 2020 at 03:48):

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

view this post on Zulip StackExchange Bot (Oct 07 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Oct 07 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Oct 07 2020 at 14:51):

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

view this post on Zulip StackExchange Bot (Oct 08 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Oct 09 2020 at 00:48):

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

view this post on Zulip StackExchange Bot (Oct 09 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Oct 10 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Oct 10 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Oct 11 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Oct 11 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Oct 11 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Oct 12 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Oct 15 2020 at 03:48):

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

view this post on Zulip StackExchange Bot (Oct 15 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Oct 15 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Oct 16 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Oct 16 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Oct 16 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Oct 17 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Oct 18 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Oct 18 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Oct 21 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Oct 21 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Oct 22 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Oct 23 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Oct 24 2020 at 03:48):

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

view this post on Zulip StackExchange Bot (Oct 26 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Oct 27 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Oct 27 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Oct 28 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Nov 03 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Nov 03 2020 at 22:48):

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

view this post on Zulip StackExchange Bot (Nov 04 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Nov 04 2020 at 23:49):

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

view this post on Zulip StackExchange Bot (Nov 07 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Nov 08 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Nov 09 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Nov 09 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Nov 09 2020 at 16:51):

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

view this post on Zulip StackExchange Bot (Nov 09 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Nov 11 2020 at 02:48):

blaineh posted a new question on November 11, 2020 at 03:09AM: match goal doesn't match let destructuring expression – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 11 2020 at 12:48):

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

view this post on Zulip StackExchange Bot (Nov 11 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Nov 12 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Nov 12 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Nov 14 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Nov 14 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Nov 15 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Nov 15 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Nov 17 2020 at 02:48):

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

view this post on Zulip StackExchange Bot (Nov 17 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Nov 17 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Nov 19 2020 at 00:48):

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

view this post on Zulip StackExchange Bot (Nov 19 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Nov 20 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Nov 20 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Nov 21 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Nov 22 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Nov 23 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Nov 26 2020 at 10:48):

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

view this post on Zulip StackExchange Bot (Nov 27 2020 at 00:48):

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

view this post on Zulip StackExchange Bot (Nov 27 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Nov 30 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Dec 01 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Dec 02 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Dec 03 2020 at 06:48):

gust posted a new question on December 03, 2020 at 07:07AM: coqc -Qreturns "coqc: -Q: no such file or directory" – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 03 2020 at 09:48):

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

view this post on Zulip StackExchange Bot (Dec 03 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Dec 04 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Dec 04 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Dec 04 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Dec 06 2020 at 07:48):

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

view this post on Zulip StackExchange Bot (Dec 06 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Dec 07 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Dec 10 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Dec 11 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Dec 11 2020 at 11:48):

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

view this post on Zulip StackExchange Bot (Dec 11 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Dec 13 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Dec 15 2020 at 20:48):

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

view this post on Zulip StackExchange Bot (Dec 17 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Dec 19 2020 at 04:48):

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

view this post on Zulip StackExchange Bot (Dec 19 2020 at 04:48):

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

view this post on Zulip StackExchange Bot (Dec 21 2020 at 14:48):

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

view this post on Zulip StackExchange Bot (Dec 21 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Dec 21 2020 at 21:48):

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

view this post on Zulip StackExchange Bot (Dec 22 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Dec 23 2020 at 05:48):

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

view this post on Zulip StackExchange Bot (Dec 23 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Dec 24 2020 at 19:48):

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

view this post on Zulip StackExchange Bot (Dec 25 2020 at 06:48):

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

view this post on Zulip StackExchange Bot (Dec 28 2020 at 08:48):

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

view this post on Zulip StackExchange Bot (Dec 29 2020 at 15:48):

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

view this post on Zulip StackExchange Bot (Dec 29 2020 at 17:48):

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

view this post on Zulip StackExchange Bot (Dec 30 2020 at 03:48):

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

view this post on Zulip StackExchange Bot (Dec 30 2020 at 13:48):

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

view this post on Zulip StackExchange Bot (Dec 30 2020 at 16:48):

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

view this post on Zulip StackExchange Bot (Jan 06 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Jan 06 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Jan 06 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jan 07 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Jan 08 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jan 09 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Jan 10 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Jan 14 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jan 14 2021 at 15:48):

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

view this post on Zulip StackExchange Bot (Jan 16 2021 at 06:48):

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

view this post on Zulip StackExchange Bot (Jan 16 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Jan 17 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jan 19 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Jan 20 2021 at 02:48):

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

view this post on Zulip StackExchange Bot (Jan 20 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Jan 20 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jan 22 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Jan 23 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (Jan 24 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Jan 26 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Jan 26 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Jan 28 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Jan 28 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Jan 29 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jan 31 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Jan 31 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Feb 02 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Feb 02 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Feb 02 2021 at 15:48):

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

view this post on Zulip StackExchange Bot (Feb 03 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Feb 04 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Feb 04 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Feb 05 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Feb 05 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Feb 07 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Feb 11 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Feb 11 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Feb 12 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Feb 14 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Feb 16 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Feb 16 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Feb 17 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Feb 18 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Feb 20 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Feb 20 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Feb 23 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Feb 27 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Feb 27 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Feb 28 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Mar 01 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Mar 03 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Mar 04 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Mar 04 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Mar 06 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Mar 07 2021 at 01:48):

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

view this post on Zulip StackExchange Bot (Mar 07 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Mar 11 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Mar 13 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Mar 14 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Mar 15 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Mar 15 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Mar 16 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Mar 16 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Mar 16 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Mar 17 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Mar 17 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Mar 19 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Mar 19 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Mar 19 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Mar 20 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Mar 22 2021 at 15:48):

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

view this post on Zulip StackExchange Bot (Mar 22 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Mar 26 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Mar 26 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Mar 27 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Mar 28 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Mar 28 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Mar 28 2021 at 13:53):

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

view this post on Zulip StackExchange Bot (Mar 28 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Mar 29 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Mar 30 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (Mar 30 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (Mar 30 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Mar 31 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Mar 31 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (Apr 01 2021 at 02:48):

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

view this post on Zulip StackExchange Bot (Apr 01 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Apr 02 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (Apr 02 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Apr 03 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Apr 04 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Apr 06 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Apr 07 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Apr 08 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Apr 08 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Apr 08 2021 at 16:49):

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

view this post on Zulip StackExchange Bot (Apr 08 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Apr 08 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Apr 09 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Apr 09 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Apr 10 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Apr 10 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Apr 13 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Apr 14 2021 at 15:48):

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

view this post on Zulip StackExchange Bot (Apr 15 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Apr 16 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Apr 17 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Apr 18 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Apr 19 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Apr 19 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Apr 20 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Apr 20 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Apr 20 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Apr 20 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Apr 21 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Apr 26 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Apr 27 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Apr 27 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Apr 27 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Apr 28 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Apr 29 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (Apr 29 2021 at 21:51):

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

view this post on Zulip StackExchange Bot (Apr 30 2021 at 20:48):

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

view this post on Zulip StackExchange Bot (May 01 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (May 01 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (May 03 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (May 04 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (May 11 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (May 14 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (May 16 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (May 17 2021 at 08:48):

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

view this post on Zulip StackExchange Bot (May 17 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (May 21 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (May 22 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (May 22 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (May 23 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (May 23 2021 at 15:48):

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

view this post on Zulip StackExchange Bot (May 23 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (May 24 2021 at 00:48):

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

view this post on Zulip StackExchange Bot (May 24 2021 at 02:48):

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

view this post on Zulip StackExchange Bot (May 24 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (May 25 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (May 28 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (May 30 2021 at 06:48):

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

view this post on Zulip StackExchange Bot (Jun 04 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 09 2021 at 13:48):

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

view this post on Zulip StackExchange Bot (Jun 11 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Jun 12 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Jun 13 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 13 2021 at 21:48):

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

view this post on Zulip StackExchange Bot (Jun 15 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Jun 15 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Jun 17 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Jun 18 2021 at 01:48):

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

view this post on Zulip StackExchange Bot (Jun 18 2021 at 19:48):

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

view this post on Zulip Andrey Klaus (Jun 19 2021 at 07:41):

https://stackoverflow.com/questions/68044580/why-unable-to-perform-case-analysis-in-rather-simple-case

view this post on Zulip StackExchange Bot (Jun 19 2021 at 07:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 01:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 14:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Jun 20 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Jun 21 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Jun 21 2021 at 22:48):

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

view this post on Zulip StackExchange Bot (Jun 22 2021 at 01:48):

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

view this post on Zulip StackExchange Bot (Jun 22 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 22 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 22 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jun 22 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jun 23 2021 at 02:48):

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

view this post on Zulip StackExchange Bot (Jun 23 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Jun 23 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Jun 23 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Jun 24 2021 at 01:48):

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

view this post on Zulip StackExchange Bot (Jun 24 2021 at 18:48):

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

view this post on Zulip StackExchange Bot (Jun 24 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Jun 24 2021 at 23:48):

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

view this post on Zulip StackExchange Bot (Jun 25 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jun 26 2021 at 11:48):

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

view this post on Zulip StackExchange Bot (Jun 28 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jun 28 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Jun 30 2021 at 19:48):

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

view this post on Zulip StackExchange Bot (Jul 02 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 04 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jul 04 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jul 04 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 07 2021 at 04:48):

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

view this post on Zulip StackExchange Bot (Jul 08 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Jul 08 2021 at 05:48):

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

view this post on Zulip StackExchange Bot (Jul 08 2021 at 09:48):

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

view this post on Zulip StackExchange Bot (Jul 09 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 10 2021 at 06:48):

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

view this post on Zulip StackExchange Bot (Jul 10 2021 at 16:48):

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

view this post on Zulip StackExchange Bot (Jul 10 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 11 2021 at 03:48):

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

view this post on Zulip StackExchange Bot (Jul 11 2021 at 10:48):

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

view this post on Zulip StackExchange Bot (Jul 11 2021 at 17:48):

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

view this post on Zulip StackExchange Bot (Jul 14 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Jul 16 2021 at 12:48):

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

view this post on Zulip StackExchange Bot (Jul 18 2021 at 13:22):

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

view this post on Zulip StackExchange Bot (Jul 21 2021 at 06:22):

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

view this post on Zulip StackExchange Bot (Jul 21 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Jul 21 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Jul 23 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Jul 24 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Jul 27 2021 at 19:44):

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

view this post on Zulip StackExchange Bot (Jul 28 2021 at 15:47):

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

view this post on Zulip StackExchange Bot (Aug 01 2021 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 07 2021 at 04:44):

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

view this post on Zulip StackExchange Bot (Aug 07 2021 at 07:47):

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

view this post on Zulip StackExchange Bot (Aug 09 2021 at 05:45):

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

view this post on Zulip StackExchange Bot (Aug 11 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Aug 18 2021 at 16:45):

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

view this post on Zulip StackExchange Bot (Aug 18 2021 at 18:45):

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

view this post on Zulip StackExchange Bot (Aug 18 2021 at 20:45):

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

view this post on Zulip StackExchange Bot (Aug 21 2021 at 07:44):

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

view this post on Zulip StackExchange Bot (Aug 21 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Aug 22 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Aug 24 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Aug 25 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Aug 26 2021 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 27 2021 at 12:44):

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

view this post on Zulip StackExchange Bot (Aug 27 2021 at 19:47):

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

view this post on Zulip StackExchange Bot (Aug 30 2021 at 23:45):

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

view this post on Zulip StackExchange Bot (Aug 31 2021 at 22:47):

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

view this post on Zulip StackExchange Bot (Sep 02 2021 at 18:45):

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

view this post on Zulip StackExchange Bot (Sep 05 2021 at 06:44):

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

view this post on Zulip StackExchange Bot (Sep 05 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Sep 05 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Sep 06 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Sep 07 2021 at 07:44):

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

view this post on Zulip StackExchange Bot (Sep 08 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Sep 08 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Sep 08 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Sep 08 2021 at 23:44):

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

view this post on Zulip StackExchange Bot (Sep 10 2021 at 23:44):

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

view this post on Zulip StackExchange Bot (Sep 11 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Sep 13 2021 at 00:44):

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

view this post on Zulip StackExchange Bot (Sep 13 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Sep 13 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Sep 15 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Sep 16 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Sep 17 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Sep 19 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Sep 20 2021 at 05:44):

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

view this post on Zulip StackExchange Bot (Sep 20 2021 at 06:44):

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

view this post on Zulip StackExchange Bot (Sep 21 2021 at 05:44):

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

view this post on Zulip StackExchange Bot (Sep 23 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Sep 24 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Sep 24 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Sep 25 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Sep 27 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Sep 27 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Sep 27 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Sep 28 2021 at 01:44):

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

view this post on Zulip StackExchange Bot (Sep 28 2021 at 11:44):

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

view this post on Zulip StackExchange Bot (Sep 29 2021 at 10:44):

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

view this post on Zulip StackExchange Bot (Oct 01 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Oct 01 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Oct 02 2021 at 05:44):

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

view this post on Zulip StackExchange Bot (Oct 02 2021 at 18:44):

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

view this post on Zulip StackExchange Bot (Oct 03 2021 at 16:44):

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

view this post on Zulip StackExchange Bot (Oct 04 2021 at 07:44):

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

view this post on Zulip StackExchange Bot (Oct 04 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Oct 04 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Oct 05 2021 at 12:44):

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

view this post on Zulip StackExchange Bot (Oct 05 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Oct 05 2021 at 22:45):

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

view this post on Zulip StackExchange Bot (Oct 05 2021 at 23:44):

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

view this post on Zulip StackExchange Bot (Oct 07 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Oct 10 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Oct 12 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Oct 13 2021 at 14:45):

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

view this post on Zulip StackExchange Bot (Oct 16 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Oct 17 2021 at 18:44):

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

view this post on Zulip StackExchange Bot (Oct 18 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Oct 19 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Oct 19 2021 at 16:44):

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

view this post on Zulip StackExchange Bot (Oct 20 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Oct 21 2021 at 02:44):

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

view this post on Zulip StackExchange Bot (Oct 21 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Oct 22 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Oct 25 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Oct 27 2021 at 12:44):

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

view this post on Zulip StackExchange Bot (Oct 27 2021 at 16:44):

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

view this post on Zulip StackExchange Bot (Oct 28 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Oct 29 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Oct 29 2021 at 19:44):

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

view this post on Zulip StackExchange Bot (Oct 30 2021 at 10:44):

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

view this post on Zulip StackExchange Bot (Nov 01 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Nov 02 2021 at 18:44):

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

view this post on Zulip StackExchange Bot (Nov 03 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Nov 03 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Nov 05 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Nov 05 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Nov 07 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Nov 09 2021 at 03:45):

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

view this post on Zulip StackExchange Bot (Nov 10 2021 at 17:45):

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

view this post on Zulip StackExchange Bot (Nov 11 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Nov 12 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Nov 12 2021 at 22:46):

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

view this post on Zulip StackExchange Bot (Nov 13 2021 at 18:44):

მამუკა ჯიბლაძე 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

view this post on Zulip StackExchange Bot (Nov 15 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Nov 17 2021 at 04:45):

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

view this post on Zulip StackExchange Bot (Nov 17 2021 at 08:44):

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

view this post on Zulip StackExchange Bot (Nov 17 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Nov 17 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Nov 19 2021 at 22:45):

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

view this post on Zulip StackExchange Bot (Nov 20 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Nov 20 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Nov 23 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Nov 23 2021 at 17:46):

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

view this post on Zulip StackExchange Bot (Nov 24 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Nov 25 2021 at 14:44):

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

view this post on Zulip StackExchange Bot (Nov 25 2021 at 16:45):

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

view this post on Zulip StackExchange Bot (Nov 28 2021 at 07:44):

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

view this post on Zulip StackExchange Bot (Nov 29 2021 at 16:44):

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

view this post on Zulip StackExchange Bot (Nov 29 2021 at 19:44):

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

view this post on Zulip StackExchange Bot (Nov 29 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Nov 30 2021 at 19:44):

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

view this post on Zulip StackExchange Bot (Dec 01 2021 at 01:44):

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

view this post on Zulip StackExchange Bot (Dec 01 2021 at 20:44):

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

view this post on Zulip StackExchange Bot (Dec 02 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Dec 05 2021 at 18:44):

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

view this post on Zulip StackExchange Bot (Dec 08 2021 at 12:44):

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

view this post on Zulip StackExchange Bot (Dec 08 2021 at 17:44):

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

view this post on Zulip StackExchange Bot (Dec 09 2021 at 02:45):

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

view this post on Zulip StackExchange Bot (Dec 09 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Dec 11 2021 at 23:44):

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

view this post on Zulip StackExchange Bot (Dec 12 2021 at 16:44):

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

view this post on Zulip StackExchange Bot (Dec 15 2021 at 13:44):

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

view this post on Zulip StackExchange Bot (Dec 15 2021 at 14:45):

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

view this post on Zulip StackExchange Bot (Dec 15 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Dec 16 2021 at 10:44):

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

view this post on Zulip StackExchange Bot (Dec 17 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Dec 17 2021 at 15:45):

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

view this post on Zulip StackExchange Bot (Dec 17 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Dec 18 2021 at 10:44):

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

view this post on Zulip StackExchange Bot (Dec 21 2021 at 07:44):

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

view this post on Zulip StackExchange Bot (Dec 21 2021 at 19:44):

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

view this post on Zulip StackExchange Bot (Dec 21 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Dec 22 2021 at 15:45):

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

view this post on Zulip StackExchange Bot (Dec 25 2021 at 09:44):

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

view this post on Zulip StackExchange Bot (Dec 25 2021 at 10:44):

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

view this post on Zulip StackExchange Bot (Dec 25 2021 at 22:44):

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

view this post on Zulip StackExchange Bot (Dec 27 2021 at 00:44):

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

view this post on Zulip StackExchange Bot (Dec 27 2021 at 00:44):

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

view this post on Zulip StackExchange Bot (Dec 28 2021 at 15:44):

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

view this post on Zulip StackExchange Bot (Dec 28 2021 at 21:44):

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

view this post on Zulip StackExchange Bot (Dec 29 2021 at 00:44):

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

view this post on Zulip StackExchange Bot (Dec 29 2021 at 03:44):

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

view this post on Zulip StackExchange Bot (Jan 01 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Jan 05 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Jan 06 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Jan 08 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Jan 08 2022 at 05:44):

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

view this post on Zulip StackExchange Bot (Jan 13 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Jan 14 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Jan 16 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Jan 18 2022 at 09:44):

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

view this post on Zulip StackExchange Bot (Jan 20 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Jan 20 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jan 23 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (Jan 23 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Jan 23 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Jan 24 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Jan 27 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Jan 27 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jan 28 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Jan 29 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jan 29 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Feb 01 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Feb 03 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Feb 05 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Feb 05 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Feb 05 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Feb 07 2022 at 19:46):

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

view this post on Zulip StackExchange Bot (Feb 07 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Feb 08 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Feb 11 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Feb 14 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Feb 16 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Feb 18 2022 at 19:49):

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

view this post on Zulip StackExchange Bot (Feb 21 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Feb 21 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Feb 22 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Feb 22 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Feb 22 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Feb 24 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Feb 25 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Feb 26 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Feb 26 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Feb 28 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Mar 01 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Mar 02 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Mar 02 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Mar 03 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Mar 03 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Mar 04 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 04 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 04 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 05 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Mar 07 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 08 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Mar 08 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Mar 09 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Mar 10 2022 at 20:55):

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

view this post on Zulip StackExchange Bot (Mar 11 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 12 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Mar 12 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Mar 13 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Mar 14 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 14 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 16 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Mar 16 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Mar 16 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Mar 17 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 17 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 17 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 17 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Mar 17 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Mar 18 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Mar 18 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Mar 19 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Mar 19 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Mar 19 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Mar 19 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Mar 20 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Mar 23 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 23 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Mar 23 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Mar 23 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Mar 24 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 26 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Mar 27 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Mar 27 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Mar 27 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 29 2022 at 21:45):

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

view this post on Zulip StackExchange Bot (Mar 29 2022 at 23:45):

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

view this post on Zulip StackExchange Bot (Mar 31 2022 at 18:37):

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

view this post on Zulip StackExchange Bot (Apr 01 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Apr 01 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 01 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Apr 05 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Apr 06 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Apr 07 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Apr 09 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Apr 11 2022 at 19:45):

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

view this post on Zulip StackExchange Bot (Apr 11 2022 at 22:45):

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

view this post on Zulip StackExchange Bot (Apr 12 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Apr 13 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Apr 13 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Apr 13 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Apr 14 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Apr 15 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Apr 15 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Apr 15 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Apr 16 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 16 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Apr 16 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Apr 16 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Apr 16 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Apr 17 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Apr 17 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Apr 18 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Apr 18 2022 at 01:44):

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

view this post on Zulip StackExchange Bot (Apr 18 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Apr 20 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 20 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Apr 20 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Apr 23 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Apr 24 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 24 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Apr 24 2022 at 17:45):

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

view this post on Zulip StackExchange Bot (Apr 24 2022 at 17:45):

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

view this post on Zulip StackExchange Bot (Apr 25 2022 at 12:46):

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

view this post on Zulip StackExchange Bot (Apr 26 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Apr 26 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Apr 27 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Apr 27 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Apr 27 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Apr 28 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 29 2022 at 17:46):

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

view this post on Zulip StackExchange Bot (Apr 30 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Apr 30 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Apr 30 2022 at 18:47):

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

view this post on Zulip StackExchange Bot (May 01 2022 at 14:10):

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

view this post on Zulip StackExchange Bot (May 01 2022 at 18:47):

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

view this post on Zulip StackExchange Bot (May 02 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (May 02 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (May 02 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (May 03 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (May 05 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (May 09 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (May 09 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (May 10 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (May 11 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (May 12 2022 at 09:46):

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

view this post on Zulip StackExchange Bot (May 13 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (May 14 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (May 14 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (May 14 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (May 14 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (May 15 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (May 15 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (May 17 2022 at 09:44):

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

view this post on Zulip StackExchange Bot (May 17 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (May 19 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (May 19 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (May 19 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (May 19 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (May 20 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (May 20 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (May 20 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (May 20 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (May 21 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (May 23 2022 at 14:44):

Александр Степанов 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

view this post on Zulip StackExchange Bot (May 24 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (May 24 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (May 25 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (May 25 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (May 26 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (May 26 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (May 29 2022 at 09:44):

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

view this post on Zulip StackExchange Bot (May 30 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (May 31 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Jun 01 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jun 01 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jun 01 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Jun 02 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jun 09 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jun 09 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jun 09 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Jun 10 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Jun 10 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Jun 11 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Jun 11 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Jun 11 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Jun 12 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jun 12 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Jun 12 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jun 12 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Jun 13 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jun 14 2022 at 12:45):

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

view this post on Zulip StackExchange Bot (Jun 14 2022 at 16:45):

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

view this post on Zulip StackExchange Bot (Jun 15 2022 at 17:50):

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

view this post on Zulip StackExchange Bot (Jun 19 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Jun 21 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Jun 22 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Jun 22 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Jun 23 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Jun 26 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Jun 27 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (Jun 27 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Jun 28 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Jun 28 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Jun 29 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jun 30 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Jul 01 2022 at 23:44):

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

view this post on Zulip StackExchange Bot (Jul 02 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Jul 02 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Jul 03 2022 at 11:44):

Lepticed posted a new question on July 03, 2022 at 12:02PM: Best way to make a relation associative in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 03 2022 at 17:44):

nobody posted a new question on July 03, 2022 at 07:31PM: Working with non-empty lists: any obviously preferrable approach? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 03 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Jul 04 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Jul 04 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Jul 04 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Jul 05 2022 at 07:44):

niha kee posted a new question on July 05, 2022 at 08:23AM: MAXIMUM VALUE OF THE LIST – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 07 2022 at 03:44):

Jacob woolcutt posted a new question on July 07, 2022 at 04:26AM: Where is the discriminate tactic defined in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 07 2022 at 20:44):

user566206 posted a new question on July 07, 2022 at 09:58PM: Cannot focus on a remaining unfocused goal in Coq – stackoverflow.com

view this post on Zulip Brando Miranda (Jul 08 2022 at 19:10):

why wasn't this one posted here? https://proofassistants.meta.stackexchange.com/questions/214/engineerings-questions-on-internal-details-of-proof-assistant-implementations-u

view this post on Zulip Karl Palmskog (Jul 08 2022 at 19:18):

the bot listens to the regular proofassistants StackExchange, and also regular StackOverflow and TCS overflow. It doesn't post meta questions.

view this post on Zulip StackExchange Bot (Jul 09 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Jul 09 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jul 10 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Jul 10 2022 at 17:44):

wrongbyte posted a new question on July 10, 2022 at 06:54PM: Understanding how pattern matching works in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 11 2022 at 08:44):

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

view this post on Zulip StackExchange Bot (Jul 12 2022 at 12:44):

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

view this post on Zulip Brando Miranda (Jul 13 2022 at 14:08):

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

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 14:55):

Indeed, the bot is very limited: it just forwards the RSS feed (so only new questions are noticed).

view this post on Zulip StackExchange Bot (Jul 13 2022 at 16:44):

BallBoy posted a new question on July 13, 2022 at 06:25PM: Basics of real numbers in mathcomp (Coq) – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 14 2022 at 18:44):

limitedeternity posted a new question on July 14, 2022 at 08:03PM: Proving enumerate(...) to range(len(...)) equality – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 14 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Jul 14 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jul 16 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Jul 17 2022 at 05:44):

Jimmy Stone posted a new question on July 17, 2022 at 07:20AM: Encoding records in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 18 2022 at 07:44):

Zazaeil posted a new question on July 18, 2022 at 09:13AM: nat -> nat uncountability proved in Coq – codereview.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 18 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Jul 18 2022 at 19:44):

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

view this post on Zulip StackExchange Bot (Jul 19 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Jul 21 2022 at 07:44):

niha kee posted a new question on July 21, 2022 at 09:13AM: Holding greater or equal relation between two terms – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 22 2022 at 21:44):

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

view this post on Zulip StackExchange Bot (Jul 23 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Jul 23 2022 at 12:44):

user251130 posted a new question on July 23, 2022 at 02:31PM: Decide equality with some predicate – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 24 2022 at 02:44):

Kyle Stemen posted a new question on July 24, 2022 at 04:41AM: Is coercion to a higher universe injective? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 26 2022 at 22:44):

quidproquo posted a new question on July 26, 2022 at 11:45PM: Learning Math Proof via Proof Assistants – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 27 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Jul 28 2022 at 16:44):

pjm posted a new question on July 28, 2022 at 05:06PM: Coq: rewriting under a pointwise_relation – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 28 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Jul 29 2022 at 04:44):

Naqib Zahid posted a new question on July 29, 2022 at 05:42AM: I have been stuck on MApp for pumping lemma – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 02 2022 at 07:44):

with-forest posted a new question on August 02, 2022 at 09:38AM: Define a function using another function – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 02 2022 at 09:44):

钱一程 posted a new question on August 02, 2022 at 11:40AM: Unexpected coercion in constant definition – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 02 2022 at 13:44):

钱一程 posted a new question on August 02, 2022 at 11:40AM: Unexpected eta expansion in constant definition – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 03 2022 at 03:44):

with-forest posted a new question on August 03, 2022 at 05:27AM: A problem similar to intermediate value problem – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 04 2022 at 07:44):

Lepticed posted a new question on August 04, 2022 at 09:42AM: How to use a definition in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 04 2022 at 09:45):

Indprinciple posted a new question on August 04, 2022 at 11:21AM: How to instantiate non-dependent implicit arguments in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 04 2022 at 11:44):

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

view this post on Zulip StackExchange Bot (Aug 07 2022 at 22:44):

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

view this post on Zulip StackExchange Bot (Aug 08 2022 at 01:44):

scubed posted a new question on August 08, 2022 at 02:10AM: Prove equality with eq_rect without UIP – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 08 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Aug 08 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Aug 10 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Aug 10 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 11 2022 at 09:44):

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

view this post on Zulip StackExchange Bot (Aug 17 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 20 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Aug 21 2022 at 20:44):

ax_fer posted a new question on August 21, 2022 at 09:58PM: Coq : replace hypothesis into implication – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 22 2022 at 03:44):

with-forest posted a new question on August 22, 2022 at 03:54AM: What is the remaining goals on the shelf? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 24 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 25 2022 at 02:44):

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

view this post on Zulip StackExchange Bot (Aug 27 2022 at 14:04):

Netchaiev posted a new question on August 27, 2022 at 03:34PM: Natural deduction with coq assistant prover – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 30 2022 at 00:47):

Pietro Braione posted a new question on August 30, 2022 at 02:04AM: How do I prove this property in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 30 2022 at 03:54):

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

view this post on Zulip StackExchange Bot (Aug 31 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Aug 31 2022 at 14:44):

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

view this post on Zulip StackExchange Bot (Sep 01 2022 at 05:44):

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

view this post on Zulip StackExchange Bot (Sep 02 2022 at 03:44):

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

view this post on Zulip StackExchange Bot (Sep 02 2022 at 16:45):

op325 posted a new question on September 02, 2022 at 05:59PM: setoid_rewrite failed with MathClasses Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 08 2022 at 12:44):

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

view this post on Zulip StackExchange Bot (Sep 11 2022 at 10:44):

nicolas posted a new question on September 11, 2022 at 12:09PM: Using proof assistants to generate fast code – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 15 2022 at 16:44):

Rincewind posted a new question on September 15, 2022 at 05:23PM: .CoqMakefile.d required by CoqMakefile but not generated – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 18 2022 at 13:44):

Taimoor Zaeem posted a new question on September 18, 2022 at 03:34PM: How do I exit coqtop REPL? – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 19 2022 at 07:44):

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

view this post on Zulip StackExchange Bot (Sep 27 2022 at 22:44):

sudgy posted a new question on September 28, 2022 at 12:35AM: Coq Typeclass on Functions Gets Confused by Equality – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 28 2022 at 09:44):

rsaill posted a new question on September 28, 2022 at 10:54AM: Using VST with GCC – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 29 2022 at 04:44):

Yu-Fang Chen posted a new question on September 29, 2022 at 06:05AM: Install why3-coq on MacBook Pro – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 04 2022 at 17:44):

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

view this post on Zulip StackExchange Bot (Oct 05 2022 at 13:44):

KingsAlpaca posted a new question on October 05, 2022 at 03:36PM: How to rearrange newly defined associative terms in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 13 2022 at 01:44):

Zak Kent posted a new question on October 13, 2022 at 03:03AM: Default Implementation of Coq typeclass methods – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 14 2022 at 16:44):

Stefan posted a new question on October 14, 2022 at 06:32PM: Proof of "less than or equal" transitive law in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 15 2022 at 02:44):

Huan Sun posted a new question on October 15, 2022 at 03:53AM: concurrent separation logic in Isabelle – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 15 2022 at 10:44):

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

view this post on Zulip StackExchange Bot (Oct 19 2022 at 15:44):

sp1ff posted a new question on October 19, 2022 at 04:19PM: How to scope Search to the current module only – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 19 2022 at 22:44):

mateus filipe posted a new question on October 19, 2022 at 11:10PM: prove DeMorgan law in coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 20 2022 at 08:44):

Dave posted a new question on October 20, 2022 at 10:37AM: Universe polymorphism and modules in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 20 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Oct 26 2022 at 20:44):

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

view this post on Zulip StackExchange Bot (Oct 27 2022 at 00:44):

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

view this post on Zulip StackExchange Bot (Nov 03 2022 at 04:44):

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

view this post on Zulip StackExchange Bot (Nov 04 2022 at 15:44):

임기정 posted a new question on November 04, 2022 at 03:16PM: To prove the unfolding lemma for some – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 05 2022 at 18:44):

Kamyar Mirzavaziri posted a new question on November 05, 2022 at 06:31PM: Definition by minimization in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 08 2022 at 13:44):

op325 posted a new question on November 08, 2022 at 01:04PM: Coq ssreflect - rewrite inside \big – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 09 2022 at 01:44):

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

view this post on Zulip Notification Bot (Nov 09 2022 at 09:46):

A message was moved from this topic to #VsCoq devs & users > VsCoq error by Karl Palmskog.

view this post on Zulip StackExchange Bot (Nov 10 2022 at 09:44):

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

view this post on Zulip StackExchange Bot (Nov 11 2022 at 06:44):

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

view this post on Zulip StackExchange Bot (Nov 16 2022 at 04:44):

Nathan posted a new question on November 16, 2022 at 04:08AM: Why are these two proofs so different? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 17 2022 at 09:44):

Åsmund Kløvstad posted a new question on November 17, 2022 at 10:08AM: Applying custom tactic in hypothesis – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 19 2022 at 09:44):

ZhangLiao posted a new question on November 19, 2022 at 10:15AM: Pirnting Coq definition without loading library – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 19 2022 at 22:44):

ZhangLiao posted a new question on November 19, 2022 at 10:15AM: Printing Coq definition without loading library – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 20 2022 at 13:44):

Moti posted a new question on November 20, 2022 at 01:58PM: Cannot open pixbuf loader module file in Windows – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 20 2022 at 13:44):

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

view this post on Zulip StackExchange Bot (Nov 24 2022 at 00:44):

Bromind posted a new question on November 24, 2022 at 12:17AM: Proving Union of Ensemble is not Empty_set – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 24 2022 at 20:44):

TonyBlabla posted a new question on November 24, 2022 at 08:29PM: Big Step Substraction – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 25 2022 at 07:44):

user20531868 posted a new question on November 25, 2022 at 07:02AM: Question about failure to match wildcard character "_" – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 25 2022 at 16:44):

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

view this post on Zulip StackExchange Bot (Nov 29 2022 at 05:44):

Huan Sun posted a new question on November 29, 2022 at 05:19AM: type variable in datatype definition – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 06 2022 at 11:46):

xmepl posted a new question on December 06, 2022 at 12:00PM: Coq Problem where i dont know how to continue – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 07 2022 at 08:45):

user1901 posted a new question on December 07, 2022 at 08:43AM: How do I prove a record related lemma? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Dec 10 2022 at 22:45):

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

view this post on Zulip StackExchange Bot (Dec 10 2022 at 23:45):

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

view this post on Zulip StackExchange Bot (Dec 11 2022 at 03:45):

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

view this post on Zulip StackExchange Bot (Dec 11 2022 at 23:46):

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

view this post on Zulip StackExchange Bot (Dec 12 2022 at 10:44):

pjm posted a new question on December 12, 2022 at 11:24AM: Coq: Unification fails with record – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 13 2022 at 13:49):

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

view this post on Zulip StackExchange Bot (Dec 18 2022 at 02:45):

Joshua Meyers posted a new question on December 18, 2022 at 03:04AM: How can I hide all proof terms? – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 18 2022 at 19:48):

limitedeternity posted a new question on December 18, 2022 at 07:48PM: Proving theorems containing bitwise operators – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 19 2022 at 23:48):

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

view this post on Zulip StackExchange Bot (Dec 21 2022 at 15:48):

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

view this post on Zulip StackExchange Bot (Dec 23 2022 at 15:44):

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

view this post on Zulip StackExchange Bot (Dec 24 2022 at 08:44):

コンピューターバカ posted a new question on December 24, 2022 at 09:15AM: induction integer record in coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 25 2022 at 05:44):

scubed posted a new question on December 25, 2022 at 06:42AM: Rewrite with variable from inner scope? – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 25 2022 at 05:44):

scubed posted a new question on December 25, 2022 at 06:43AM: Fix vs. Fix_sub – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 25 2022 at 18:44):

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

view this post on Zulip StackExchange Bot (Dec 31 2022 at 05:44):

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

view this post on Zulip StackExchange Bot (Jan 01 2023 at 19:44):

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

view this post on Zulip StackExchange Bot (Jan 04 2023 at 07:44):

scubed posted a new question on January 04, 2023 at 07:45AM: Is it possible to destruct and rewrite simultaneously? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 06 2023 at 03:44):

Travis Allison posted a new question on January 06, 2023 at 04:12AM: Exhaustiveness matching in proof objects for induction in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 07 2023 at 16:44):

Ícaro Lorran posted a new question on January 07, 2023 at 04:55PM: How do I write a summation on Coq? – cstheory.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 07 2023 at 18:44):

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

view this post on Zulip StackExchange Bot (Jan 07 2023 at 21:45):

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

view this post on Zulip StackExchange Bot (Jan 08 2023 at 17:44):

Ícaro Lorran posted a new question on January 08, 2023 at 05:13PM: How to write a summation in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 13 2023 at 03:44):

hilberts_drinking_problem posted a new question on January 13, 2023 at 03:27AM: Subsequences in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 14 2023 at 22:44):

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

view this post on Zulip StackExchange Bot (Jan 19 2023 at 22:47):

amit9oct posted a new question on January 19, 2023 at 10:55PM: Imports in multi-file Coq projects – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 20 2023 at 22:45):

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

view this post on Zulip StackExchange Bot (Jan 21 2023 at 03:44):

Andre posted a new question on January 21, 2023 at 04:24AM: Vacuously true implications in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 21 2023 at 19:45):

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

view this post on Zulip StackExchange Bot (Jan 23 2023 at 18:46):

dvr posted a new question on January 23, 2023 at 07:19PM: using addf_div for rat_numDomainType – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 23 2023 at 23:44):

dvr posted a new question on January 23, 2023 at 11:13PM: Understanding \is a unit in ssreflect – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 24 2023 at 20:46):

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

view this post on Zulip StackExchange Bot (Jan 24 2023 at 22:47):

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

view this post on Zulip StackExchange Bot (Jan 26 2023 at 00:49):

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

view this post on Zulip StackExchange Bot (Jan 28 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Jan 28 2023 at 22:45):

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

view this post on Zulip StackExchange Bot (Jan 29 2023 at 20:44):

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

view this post on Zulip StackExchange Bot (Jan 30 2023 at 22:03):

Adrian L posted a new question on January 30, 2023 at 10:08PM: Destruction of bound dependent types – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 31 2023 at 20:46):

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

view this post on Zulip StackExchange Bot (Feb 01 2023 at 21:46):

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

view this post on Zulip StackExchange Bot (Feb 02 2023 at 15:47):

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

view this post on Zulip StackExchange Bot (Feb 03 2023 at 08:44):

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

view this post on Zulip StackExchange Bot (Feb 07 2023 at 07:44):

greg. posted a new question on February 07, 2023 at 07:20AM: Lean4: Proving that (xs = ys) = (reverse xs = reverse ys) – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 08 2023 at 09:44):

footnotes posted a new question on February 08, 2023 at 10:23AM: How to prove A \/ False -> A in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 08 2023 at 18:44):

larsr posted a new question on February 08, 2023 at 06:38PM: How does one expand a fix function just one step? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 10 2023 at 18:44):

matteo_c posted a new question on February 10, 2023 at 06:56PM: Stream of all finite prefixes of a stream – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 11 2023 at 03:44):

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

view this post on Zulip StackExchange Bot (Feb 12 2023 at 11:44):

Bruno posted a new question on February 10, 2023 at 11:07AM: Why does Ltac not match the clause? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 13 2023 at 17:44):

matteo_c posted a new question on February 13, 2023 at 06:23PM: Two-step induction of inductive predicate on Streams – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 13 2023 at 21:44):

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

view this post on Zulip StackExchange Bot (Feb 14 2023 at 00:44):

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

view this post on Zulip StackExchange Bot (Feb 14 2023 at 18:44):

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

view this post on Zulip StackExchange Bot (Feb 14 2023 at 20:44):

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

view this post on Zulip StackExchange Bot (Feb 15 2023 at 19:44):

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

view this post on Zulip StackExchange Bot (Feb 15 2023 at 21:44):

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

view this post on Zulip StackExchange Bot (Feb 15 2023 at 23:44):

massive coq posted a new question on February 15, 2023 at 11:49PM: Coq abilities and usage – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 16 2023 at 14:44):

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

view this post on Zulip StackExchange Bot (Feb 17 2023 at 18:44):

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

view this post on Zulip StackExchange Bot (Feb 17 2023 at 21:44):

user2506946 posted a new question on February 17, 2023 at 09:58PM: How to overload the "+" notation in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 22 2023 at 23:03):

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

view this post on Zulip StackExchange Bot (Feb 23 2023 at 15:44):

M B posted a new question on February 23, 2023 at 04:34PM: Program Fixpoint decreasing on measure produces unsolvable goal – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 23 2023 at 17:44):

Coqerellen posted a new question on February 23, 2023 at 05:32PM: Destructing transitivity hypothesis on simple predicate logic – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 05 2023 at 00:44):

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

view this post on Zulip StackExchange Bot (Mar 07 2023 at 15:44):

asha soroushpoor posted a new question on March 07, 2023 at 03:39PM: Coq Induction on Hypothesis destroys the Hypothesis – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 10 2023 at 19:44):

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

view this post on Zulip StackExchange Bot (Mar 11 2023 at 10:44):

user65526 posted a new question on March 11, 2023 at 10:45AM: Understanding a message on CoqIde – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 11 2023 at 12:44):

user65526 posted a new question on March 11, 2023 at 01:22PM: Complete Atomic Boolean algebras in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 11 2023 at 14:44):

user65526 posted a new question on March 11, 2023 at 02:53PM: Activating nested proof – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 11 2023 at 18:44):

user65526 posted a new question on March 11, 2023 at 05:49PM: Definite description operator in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 14 2023 at 08:44):

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

view this post on Zulip StackExchange Bot (Mar 14 2023 at 11:44):

user65526 posted a new question on March 14, 2023 at 11:42AM: Unclear error message regarding format and notation – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 14 2023 at 16:44):

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

view this post on Zulip StackExchange Bot (Mar 15 2023 at 15:44):

radrow posted a new question on March 15, 2023 at 04:20PM: How to create a custom Ltac to recursively destruct conjunctions? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 20 2023 at 12:44):

user65526 posted a new question on March 20, 2023 at 01:20PM: Disjunction and the error `No product after head reduction' – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 20 2023 at 18:44):

Felipe posted a new question on March 20, 2023 at 06:14PM: How to reason about equality between different datatypes? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 20 2023 at 21:44):

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

view this post on Zulip StackExchange Bot (Mar 21 2023 at 06:44):

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

view this post on Zulip StackExchange Bot (Mar 21 2023 at 08:44):

Lepticed posted a new question on March 21, 2023 at 09:19AM: How to distribute an AND operator in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 21 2023 at 16:44):

user65526 posted a new question on March 21, 2023 at 04:39PM: A proof by cases – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 21 2023 at 17:44):

user65526 posted a new question on March 21, 2023 at 04:39PM: The apply rule in proof by cases – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 22 2023 at 11:44):

anurag posted a new question on March 22, 2023 at 11:59AM: How to formally verify a compiler (frontend and/or backend)? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 22 2023 at 11:44):

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

view this post on Zulip StackExchange Bot (Mar 23 2023 at 04:44):

sudgy posted a new question on March 23, 2023 at 04:24AM: Rewrite with definitional equality and dependent types – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 23 2023 at 08:44):

コンピューターバカ posted a new question on March 23, 2023 at 08:35AM: How to use induction tactic on recursively defined functions in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 24 2023 at 01:44):

コンピューターバカ posted a new question on March 23, 2023 at 08:35AM: How to proof recursively defined functions' prop in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 25 2023 at 13:44):

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

view this post on Zulip StackExchange Bot (Mar 25 2023 at 18:44):

Mohan Radhakrishnan posted a new question on March 25, 2023 at 06:31PM: 'coqc' does not find findlib.conf – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 30 2023 at 10:44):

Lepticed posted a new question on March 30, 2023 at 12:06PM: How can I better structure Coq files? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 30 2023 at 11:44):

Lepticed posted a new question on March 30, 2023 at 01:31PM: How to deal with lemma only used once in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 31 2023 at 14:44):

pjm posted a new question on March 31, 2023 at 02:54PM: Morphism signature for dependently-typed vectors in coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 01 2023 at 00:44):

Lepticed posted a new question on April 01, 2023 at 01:32AM: How to write the iota descriptor in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 02 2023 at 20:44):

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

view this post on Zulip StackExchange Bot (Apr 04 2023 at 05:44):

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

view this post on Zulip StackExchange Bot (Apr 05 2023 at 14:01):

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

view this post on Zulip StackExchange Bot (Apr 05 2023 at 16:16):

Lepticed posted a new question on April 05, 2023 at 05:09PM: Use the contrapositive of an hypothesis in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 12 2023 at 01:46):

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

view this post on Zulip StackExchange Bot (Apr 12 2023 at 03:44):

anonymouse 29083 posted a new question on April 12, 2023 at 04:03AM: Help solve these proofs – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 12 2023 at 08:45):

hch posted a new question on April 12, 2023 at 09:01AM: stuck trying to prove sublist of list – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 12 2023 at 08:45):

hch posted a new question on April 12, 2023 at 09:16AM: stuck trying to prove sublist of list – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 12 2023 at 12:46):

HELLOBIRD 892 posted a new question on April 12, 2023 at 04:03AM: nvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvm – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 13 2023 at 11:48):

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

view this post on Zulip StackExchange Bot (Apr 14 2023 at 07:44):

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

view this post on Zulip StackExchange Bot (Apr 14 2023 at 09:44):

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

view this post on Zulip StackExchange Bot (Apr 14 2023 at 12:44):

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

view this post on Zulip StackExchange Bot (Apr 15 2023 at 02:44):

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

view this post on Zulip StackExchange Bot (Apr 17 2023 at 00:44):

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

view this post on Zulip StackExchange Bot (Apr 17 2023 at 15:45):

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

view this post on Zulip StackExchange Bot (Apr 18 2023 at 03:44):

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

view this post on Zulip StackExchange Bot (Apr 19 2023 at 22:45):

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

view this post on Zulip StackExchange Bot (Apr 20 2023 at 14:46):

anonymous12345677654 posted a new question on April 20, 2023 at 04:03PM: Type coercions in finset – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 21 2023 at 14:46):

Felipe posted a new question on April 21, 2023 at 03:42PM: Rewriting with heterogeneous equality (JMeq) – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 22 2023 at 00:44):

Pavel Shuhray posted a new question on April 22, 2023 at 02:34AM: Dependent sum and equality with Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 24 2023 at 18:46):

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

view this post on Zulip StackExchange Bot (Apr 25 2023 at 03:44):

itsFrank posted a new question on April 25, 2023 at 05:34AM: How to solve this proof – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 25 2023 at 06:44):

itsFrank posted a new question on April 25, 2023 at 05:34AM: Hwo to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 26 2023 at 06:44):

aaay posted a new question on April 26, 2023 at 08:17AM: Recursion and Pattern matching in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 27 2023 at 10:44):

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

view this post on Zulip StackExchange Bot (Apr 27 2023 at 15:45):

itsFrank posted a new question on April 25, 2023 at 05:34AM: How to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 28 2023 at 01:45):

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

view this post on Zulip StackExchange Bot (Apr 30 2023 at 07:45):

8bc3 457f posted a new question on April 30, 2023 at 08:13AM: Inductive vs. recursive definitions – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 30 2023 at 07:45):

8bc3 457f posted a new question on April 30, 2023 at 08:22AM: Debug autorewrite in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 01 2023 at 05:45):

sudgy posted a new question on May 01, 2023 at 07:05AM: Weird use of equality in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 01 2023 at 14:46):

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

view this post on Zulip StackExchange Bot (May 02 2023 at 20:56):

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

view this post on Zulip StackExchange Bot (May 02 2023 at 22:05):

dvr posted a new question on May 02, 2023 at 11:22PM: Raising a natural number, int, or rat to a rational? – stackoverflow.com

view this post on Zulip StackExchange Bot (May 03 2023 at 12:44):

Felipe posted a new question on May 03, 2023 at 01:44PM: Reasoning about non reflexive equalities & type conversions – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 05 2023 at 20:45):

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

view this post on Zulip StackExchange Bot (May 07 2023 at 10:44):

Jay Lee posted a new question on May 07, 2023 at 12:10PM: Ltac tactic that accepts an arbitrary number of quantifiers – stackoverflow.com

view this post on Zulip StackExchange Bot (May 09 2023 at 12:45):

Bas Laarakker posted a new question on May 09, 2023 at 01:07PM: Rewriting within sigma types in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (May 10 2023 at 18:45):

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

view this post on Zulip StackExchange Bot (May 11 2023 at 10:46):

dvr posted a new question on May 11, 2023 at 12:25PM: Coerce rat to realType im math-comp/analysis – stackoverflow.com

view this post on Zulip StackExchange Bot (May 11 2023 at 21:44):

Felipe Morelli posted a new question on May 11, 2023 at 10:01PM: Help with proofs in analysis – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 13 2023 at 09:44):

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

view this post on Zulip StackExchange Bot (May 13 2023 at 21:45):

Jack posted a new question on May 13, 2023 at 11:42PM: Proof List Inequality in Coq – cstheory.stackexchange.com

view this post on Zulip StackExchange Bot (May 14 2023 at 10:44):

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

view this post on Zulip StackExchange Bot (May 15 2023 at 12:45):

shooqie posted a new question on May 15, 2023 at 02:32PM: Non-trivial Fixpoint on nested recursive types – stackoverflow.com

view this post on Zulip StackExchange Bot (May 15 2023 at 13:45):

Tilman Zuckmantel posted a new question on May 15, 2023 at 03:34PM: Importing a Module in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (May 15 2023 at 19:45):

Jeff Witnick posted a new question on May 15, 2023 at 08:23PM: Induction COQ Question – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 15 2023 at 19:45):

Jeff Witnick posted a new question on May 15, 2023 at 09:34PM: Help I am confused...Proof Assistant – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 15 2023 at 22:45):

Jeff Witnick posted a new question on May 16, 2023 at 12:42AM: Equivalence Relations COQ – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 16 2023 at 00:44):

Jeff Witnick posted a new question on May 16, 2023 at 02:21AM: Help with strong induction – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 16 2023 at 12:45):

Jeff Witnick posted a new question on May 16, 2023 at 02:33PM: Help with Divisibility and GCD – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 16 2023 at 18:45):

deleted_user0972 posted a new question on May 15, 2023 at 08:23PM: inductive COQ concern – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 16 2023 at 18:45):

randomguest0002 posted a new question on May 16, 2023 at 08:44PM: coq proof question – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 17 2023 at 04:44):

randomguest0002 posted a new question on May 16, 2023 at 08:44PM: Organizing a Coq proof – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 17 2023 at 17:44):

deleted_user0972 posted a new question on May 15, 2023 at 09:34PM: No subterm matching Hab * a – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 19 2023 at 20:45):

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

view this post on Zulip StackExchange Bot (May 20 2023 at 12:44):

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

view this post on Zulip StackExchange Bot (May 20 2023 at 19:45):

epelaez posted a new question on May 20, 2023 at 09:20PM: Replace element in Coq list – stackoverflow.com

view this post on Zulip StackExchange Bot (May 23 2023 at 22:44):

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

view this post on Zulip StackExchange Bot (May 27 2023 at 20:44):

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

view this post on Zulip StackExchange Bot (May 28 2023 at 00:44):

shooqie posted a new question on May 28, 2023 at 01:25AM: Set type Variable to a concrete type inside a definition – stackoverflow.com

view this post on Zulip StackExchange Bot (May 29 2023 at 15:44):

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

view this post on Zulip StackExchange Bot (May 30 2023 at 21:44):

epelaez posted a new question on May 30, 2023 at 09:46PM: Implementing variable replacement in a boolean polynomial function in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 01 2023 at 18:44):

coqbeginner posted a new question on June 01, 2023 at 08:35PM: Notation problem – cstheory.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 02 2023 at 15:47):

nobody posted a new question on June 02, 2023 at 04:20PM: Including header / footer in a file generated by extraction – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 02 2023 at 15:47):

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

view this post on Zulip StackExchange Bot (Jun 02 2023 at 17:47):

R. Bosman posted a new question on June 02, 2023 at 05:59PM: How to teach crush to unfold definitions? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 04 2023 at 03:44):

epelaez posted a new question on June 04, 2023 at 04:48AM: Clear hypotheses after recursive Ltac – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 05 2023 at 10:45):

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

view this post on Zulip StackExchange Bot (Jun 06 2023 at 00:44):

cosmonia posted a new question on June 06, 2023 at 02:10AM: Proving Transitivity of Pointwise Relations on Lists in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 08 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Jun 09 2023 at 04:45):

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

view this post on Zulip StackExchange Bot (Jun 13 2023 at 11:45):

Bas Laarakker posted a new question on June 13, 2023 at 12:16PM: Is Prop extensionality inconsistent in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 13 2023 at 19:45):

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

view this post on Zulip StackExchange Bot (Jun 14 2023 at 09:44):

Bruno posted a new question on June 14, 2023 at 11:35AM: Obligation generated by Equations is too strong – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 14 2023 at 19:45):

Moti posted a new question on June 14, 2023 at 08:56PM: Natural deduction in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 16 2023 at 01:44):

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

view this post on Zulip StackExchange Bot (Jun 18 2023 at 03:44):

dvr posted a new question on June 18, 2023 at 03:57AM: Domain of a map in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 22 2023 at 15:45):

Joey Eremondi posted a new question on June 22, 2023 at 05:01PM: Reasoning about CwFs in a proof assistant – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 23 2023 at 13:45):

hmltn posted a new question on June 23, 2023 at 03:35PM: What is the definition of Turing-complete in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 23 2023 at 17:45):

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

view this post on Zulip StackExchange Bot (Jun 23 2023 at 21:45):

shooqie posted a new question on June 23, 2023 at 11:19PM: Tricks for proving equalities under type cast – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jun 24 2023 at 17:45):

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

view this post on Zulip StackExchange Bot (Jun 26 2023 at 20:45):

Elad Strasman posted a new question on June 26, 2023 at 09:04PM: coq Constructive mathematics task – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 27 2023 at 01:45):

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

view this post on Zulip StackExchange Bot (Jun 27 2023 at 18:44):

radrow posted a new question on June 27, 2023 at 07:57PM: Is Prop a subtype of Set? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 29 2023 at 15:45):

yiyuan-cao posted a new question on June 29, 2023 at 04:45PM: Programming in Calculus of Inductive Constructions with Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 29 2023 at 22:45):

Lepticed posted a new question on June 30, 2023 at 12:04AM: Rewrite proposition using equivalence in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jun 30 2023 at 02:45):

yiyuan-cao posted a new question on June 29, 2023 at 04:45PM: Programming in the Calculus of Inductive Constructions with Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 08 2023 at 06:44):

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

view this post on Zulip StackExchange Bot (Jul 09 2023 at 20:44):

shooqie posted a new question on July 09, 2023 at 09:17PM: Ltac - run tactic for each hypothesis of given pattern – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 12 2023 at 07:45):

Pietro Braione posted a new question on July 12, 2023 at 09:14AM: How do I debug Gallina (Coq) code? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 12 2023 at 10:45):

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

view this post on Zulip StackExchange Bot (Jul 12 2023 at 15:45):

matteo_c posted a new question on July 12, 2023 at 05:17PM: Induction error on mutually defined types in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 12 2023 at 17:44):

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

view this post on Zulip StackExchange Bot (Jul 14 2023 at 11:45):

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

view this post on Zulip StackExchange Bot (Jul 16 2023 at 13:45):

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

view this post on Zulip StackExchange Bot (Jul 16 2023 at 15:45):

uhbif19 posted a new question on July 16, 2023 at 04:34PM: Formalization of matching logic (logic behind K Framework) – cstheory.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 16 2023 at 17:45):

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

view this post on Zulip StackExchange Bot (Jul 16 2023 at 19:45):

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

view this post on Zulip StackExchange Bot (Jul 16 2023 at 19:45):

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

view this post on Zulip StackExchange Bot (Jul 17 2023 at 16:45):

Pandemonium posted a new question on July 17, 2023 at 05:45PM: Unable to unify "n * 0" with "0" – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 20 2023 at 01:44):

L-- posted a new question on July 20, 2023 at 02:55AM: PLF: [S <: S->S] Subtyping Example Hint – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 20 2023 at 16:44):

Lepticed posted a new question on July 20, 2023 at 05:57PM: Coq: A \/ A -> A – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 21 2023 at 15:45):

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

view this post on Zulip StackExchange Bot (Jul 22 2023 at 10:45):

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

view this post on Zulip StackExchange Bot (Jul 25 2023 at 09:45):

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

view this post on Zulip StackExchange Bot (Jul 29 2023 at 06:45):

toku-sa-n posted a new question on July 29, 2023 at 07:27AM: How to extract the exact information of GenArg? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jul 31 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Jul 31 2023 at 20:46):

Julián posted a new question on July 31, 2023 at 10:03PM: Have Hyperdoctrines been formalized? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 01 2023 at 03:45):

Agnishom Chattopadhyay posted a new question on August 01, 2023 at 04:50AM: Rewriting inside quantified propositions in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 02 2023 at 20:44):

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

view this post on Zulip StackExchange Bot (Aug 03 2023 at 19:44):

Lepticed posted a new question on August 03, 2023 at 07:48PM: Forall and exists in a Coq proof – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 08 2023 at 15:44):

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

view this post on Zulip StackExchange Bot (Aug 08 2023 at 15:44):

Vladimir Prigodsky posted a new question on August 08, 2023 at 05:14PM: Using CoqHammer from Ltac2 – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 09 2023 at 01:44):

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

view this post on Zulip StackExchange Bot (Aug 11 2023 at 12:45):

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

view this post on Zulip StackExchange Bot (Aug 12 2023 at 15:46):

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

view this post on Zulip StackExchange Bot (Aug 12 2023 at 19:46):

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

view this post on Zulip StackExchange Bot (Aug 15 2023 at 09:44):

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

view this post on Zulip StackExchange Bot (Aug 15 2023 at 09:44):

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

view this post on Zulip StackExchange Bot (Aug 15 2023 at 14:45):

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

view this post on Zulip StackExchange Bot (Aug 16 2023 at 12:45):

vzhilin posted a new question on August 16, 2023 at 02:32PM: List without gaps in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 16 2023 at 20:46):

Nicolas Rinaudo posted a new question on August 16, 2023 at 10:29PM: Force Coq to simplify unfalsifiable pattern matches – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 17 2023 at 12:44):

userl6kgPo0ixv posted a new question on August 17, 2023 at 01:28PM: Proving function existence in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 17 2023 at 12:44):

noCrayCray posted a new question on August 17, 2023 at 02:31PM: İnduction/inversion and others in coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 17 2023 at 19:46):

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

view this post on Zulip StackExchange Bot (Aug 19 2023 at 10:46):

E030E03 posted a new question on August 19, 2023 at 11:54AM: Coq specifying the type of a variable – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 23 2023 at 12:46):

joro posted a new question on August 23, 2023 at 02:31PM: How bad is Coq proving both $T$ and $\lnot T$? – mathoverflow.net

view this post on Zulip StackExchange Bot (Aug 24 2023 at 18:44):

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

view this post on Zulip StackExchange Bot (Aug 26 2023 at 21:46):

arshiamoeini posted a new question on August 26, 2023 at 10:52PM: formalization of partial function for counting – cs.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 27 2023 at 15:47):

arshiamoeini posted a new question on August 27, 2023 at 04:47PM: formalization of partial function for counting – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 27 2023 at 19:45):

arshiamoeini posted a new question on August 27, 2023 at 04:47PM: Formalization of partial functions for combinatorial counting – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Aug 29 2023 at 23:45):

acogrunge posted a new question on August 30, 2023 at 01:15AM: false = true problem when solving Lemma in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Aug 31 2023 at 19:44):

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

view this post on Zulip StackExchange Bot (Sep 01 2023 at 07:45):

Andrii Kozytskyi posted a new question on September 01, 2023 at 09:08AM: Specializing forall quantifiers in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 05 2023 at 16:44):

Circuit Craft posted a new question on September 05, 2023 at 06:21PM: Eliminating dependent destruction in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 06 2023 at 16:46):

noCrayCray posted a new question on September 06, 2023 at 05:12PM: confused about stlc from Programming Language Foundations – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Sep 07 2023 at 11:45):

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

view this post on Zulip StackExchange Bot (Sep 10 2023 at 05:44):

kunkun posted a new question on September 10, 2023 at 07:03AM: How to proof by natural number case analysis in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 11 2023 at 23:46):

user3598542 posted a new question on September 12, 2023 at 12:40AM: How to represent 2D array in Verifiable C – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 12 2023 at 06:45):

user1953221 posted a new question on September 12, 2023 at 08:22AM: Understanding TLC's finite map library – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 14 2023 at 16:46):

jschroed TV posted a new question on September 14, 2023 at 05:57PM: vscoq language server failed installing – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 19 2023 at 12:45):

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

view this post on Zulip StackExchange Bot (Sep 19 2023 at 16:45):

someStudentCS posted a new question on September 19, 2023 at 06:36PM: Coq: Cannot infer the type of function in environment – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 20 2023 at 08:46):

someStudentCS posted a new question on September 19, 2023 at 06:36PM: Cannot infer the type of function in environment – stackoverflow.com

view this post on Zulip StackExchange Bot (Sep 21 2023 at 17:46):

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

view this post on Zulip StackExchange Bot (Sep 26 2023 at 05:44):

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

view this post on Zulip StackExchange Bot (Sep 29 2023 at 01:44):

Michael Hennebry posted a new question on September 29, 2023 at 02:47AM: gappa seems to generate bad Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 01 2023 at 19:45):

Jon posted a new question on October 01, 2023 at 08:00PM: Eta-equality for records: the case of semigroups – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 03 2023 at 14:46):

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

view this post on Zulip StackExchange Bot (Oct 05 2023 at 20:46):

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

view this post on Zulip StackExchange Bot (Oct 10 2023 at 21:46):

Adrian L posted a new question on October 10, 2023 at 10:39PM: Use proof irrelevance in cast – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 12 2023 at 13:45):

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

view this post on Zulip StackExchange Bot (Oct 16 2023 at 16:47):

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

view this post on Zulip StackExchange Bot (Oct 16 2023 at 22:48):

Drona Nagarajan posted a new question on October 17, 2023 at 12:04AM: Forward leads to stack-overflow – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 18 2023 at 06:46):

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

view this post on Zulip StackExchange Bot (Oct 19 2023 at 09:46):

Jon posted a new question on October 19, 2023 at 10:57AM: Universe polymorphism and Coq standard library – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 20 2023 at 14:47):

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

view this post on Zulip StackExchange Bot (Oct 21 2023 at 03:46):

bluesquare posted a new question on October 21, 2023 at 04:25AM: True in Goal State Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 26 2023 at 19:44):

7Orion7 posted a new question on October 26, 2023 at 09:36PM: Can't find Lemma for set equality in stdpp library – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 27 2023 at 09:46):

7Orion7 posted a new question on October 27, 2023 at 11:34AM: Custom tactics provided by libraries – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 28 2023 at 12:44):

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

view this post on Zulip StackExchange Bot (Oct 29 2023 at 23:47):

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

view this post on Zulip StackExchange Bot (Oct 30 2023 at 15:44):

Felipe posted a new question on October 30, 2023 at 03:27PM: Problem working with FMapWeakList and Parametrized Records – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Oct 31 2023 at 08:46):

Drona Nagarajan posted a new question on October 31, 2023 at 09:06AM: Unable to proceed with list induction – stackoverflow.com

view this post on Zulip StackExchange Bot (Oct 31 2023 at 14:44):

Tempestas Ludi posted a new question on October 31, 2023 at 02:45PM: Continue a section (with context) in coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 01 2023 at 04:45):

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

view this post on Zulip StackExchange Bot (Nov 02 2023 at 10:47):

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

view this post on Zulip StackExchange Bot (Nov 05 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Nov 06 2023 at 22:45):

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

view this post on Zulip StackExchange Bot (Nov 10 2023 at 11:46):

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

view this post on Zulip StackExchange Bot (Nov 12 2023 at 11:46):

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

view this post on Zulip StackExchange Bot (Nov 16 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Nov 17 2023 at 11:46):

Andrey posted a new question on November 17, 2023 at 12:36PM: problem with unification – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Nov 18 2023 at 18:46):

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

view this post on Zulip StackExchange Bot (Nov 19 2023 at 11:46):

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

view this post on Zulip StackExchange Bot (Nov 19 2023 at 16:45):

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

view this post on Zulip StackExchange Bot (Nov 20 2023 at 22:44):

Marcus posted a new question on November 20, 2023 at 10:43PM: Coq code in LaTeX using lstcoq does not work – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 21 2023 at 10:46):

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

view this post on Zulip StackExchange Bot (Nov 22 2023 at 06:46):

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

view this post on Zulip StackExchange Bot (Nov 23 2023 at 20:45):

Marcus posted a new question on November 23, 2023 at 08:20PM: How to prove an inequality – stackoverflow.com

view this post on Zulip StackExchange Bot (Nov 27 2023 at 18:44):

bluesquare posted a new question on November 27, 2023 at 07:21PM: How do I install a library in coq? (MacOS) – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 01 2023 at 09:44):

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

view this post on Zulip StackExchange Bot (Dec 02 2023 at 19:44):

e2e4 posted a new question on December 02, 2023 at 07:50PM: Need help to prove (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅) – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 06 2023 at 02:44):

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

view this post on Zulip StackExchange Bot (Dec 06 2023 at 04:45):

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

view this post on Zulip StackExchange Bot (Dec 06 2023 at 21:46):

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

view this post on Zulip StackExchange Bot (Dec 07 2023 at 03:45):

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

view this post on Zulip StackExchange Bot (Dec 07 2023 at 14:47):

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

view this post on Zulip StackExchange Bot (Dec 07 2023 at 17:44):

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

view this post on Zulip StackExchange Bot (Dec 08 2023 at 15:48):

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

view this post on Zulip StackExchange Bot (Dec 10 2023 at 04:46):

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

view this post on Zulip StackExchange Bot (Dec 12 2023 at 06:47):

user1953221 posted a new question on December 12, 2023 at 06:52AM: Forward simulation with partial simulation relation – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Dec 15 2023 at 21:46):

someStudentCS posted a new question on December 15, 2023 at 09:10PM: Iris/Coq replacing literal – stackoverflow.com

view this post on Zulip StackExchange Bot (Dec 21 2023 at 15:44):

yiyuan-cao posted a new question on December 21, 2023 at 03:37PM: How to reason with notations directly? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Dec 22 2023 at 18:45):

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

view this post on Zulip StackExchange Bot (Dec 31 2023 at 10:44):

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

view this post on Zulip StackExchange Bot (Jan 05 2024 at 21:44):

Rand00 posted a new question on January 05, 2024 at 08:50PM: Coq / Lean endpoint for GPT actions – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 09 2024 at 05:45):

scubed posted a new question on January 09, 2024 at 06:35AM: Dependent equality with 2 different type functions – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 09 2024 at 16:45):

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

view this post on Zulip StackExchange Bot (Jan 10 2024 at 18:44):

radrow posted a new question on January 10, 2024 at 05:10PM: How to define a recursive notation with overlapping production? – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 10 2024 at 21:45):

Michael Schmidt posted a new question on January 10, 2024 at 10:39PM: How to apply constructor injectivity in the goal – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 11 2024 at 03:44):

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

view this post on Zulip StackExchange Bot (Jan 11 2024 at 05:44):

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

view this post on Zulip StackExchange Bot (Jan 12 2024 at 11:44):

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

view this post on Zulip StackExchange Bot (Jan 12 2024 at 22:44):

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

view this post on Zulip StackExchange Bot (Jan 16 2024 at 17:46):

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

view this post on Zulip StackExchange Bot (Jan 20 2024 at 15:44):

noCrayCray posted a new question on January 20, 2024 at 03:54PM: How to import unimath for coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 22 2024 at 12:44):

lottiebegnl posted a new question on January 22, 2024 at 01:38PM: Help with my project in the Coq proof assistant – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 22 2024 at 14:44):

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

view this post on Zulip StackExchange Bot (Jan 22 2024 at 16:44):

noCrayCray posted a new question on January 22, 2024 at 04:23PM: how to inductively define paths from paths using unimath – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jan 23 2024 at 19:44):

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

view this post on Zulip StackExchange Bot (Jan 24 2024 at 21:44):

lukmik posted a new question on January 24, 2024 at 09:23PM: How to prove this in CoqIDE – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 25 2024 at 11:44):

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

view this post on Zulip StackExchange Bot (Jan 25 2024 at 15:44):

Lepticed posted a new question on January 25, 2024 at 03:54PM: Proving some theorems on the function index in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 25 2024 at 18:44):

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

view this post on Zulip StackExchange Bot (Jan 27 2024 at 02:44):

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

view this post on Zulip StackExchange Bot (Jan 27 2024 at 06:44):

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

view this post on Zulip StackExchange Bot (Jan 29 2024 at 09:44):

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

view this post on Zulip StackExchange Bot (Jan 30 2024 at 01:44):

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

view this post on Zulip StackExchange Bot (Jan 30 2024 at 17:44):

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

view this post on Zulip StackExchange Bot (Jan 30 2024 at 19:44):

lukmik posted a new question on January 24, 2024 at 09:23PM: How to prove this in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Jan 31 2024 at 11:44):

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

view this post on Zulip StackExchange Bot (Feb 01 2024 at 11:44):

Lepticed posted a new question on February 01, 2024 at 12:26PM: Prove theorem about the last element of a list – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 01 2024 at 15:44):

Ulises Torrella posted a new question on February 01, 2024 at 03:58PM: Coq : Using a parametrised Type from within a Module – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 01 2024 at 19:44):

Ulises Torrella posted a new question on February 01, 2024 at 03:58PM: Coq : Using a parametrized Type from within a Module – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 01 2024 at 19:44):

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

view this post on Zulip Théo Zimmermann (Feb 03 2024 at 08:58):

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.

view this post on Zulip StackExchange Bot (Feb 09 2024 at 16:52):

calvin posted a new question on 2024-02-07T18:36:02Z: How can I handle this false = true case? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 09 2024 at 16:53):

calvin posted a new question on 2024-02-07T14:30:55Z: Why can't I destruct or discriminate here? – stackoverflow.com

view this post on Zulip Théo Zimmermann (Feb 09 2024 at 16:57):

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).

view this post on Zulip StackExchange Bot (Feb 11 2024 at 17:21):

someStudentCS posted a new question on 2024-02-11T17:17:05Z: Coq inductive not right form – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 12 2024 at 02:35):

scubed posted a new question on 2024-02-12T02:32:16Z: How do I move a let variable to a separate hypothesis? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 12 2024 at 15:20):

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

view this post on Zulip StackExchange Bot (Feb 12 2024 at 21:11):

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

view this post on Zulip StackExchange Bot (Feb 13 2024 at 22:20):

Johan Buret posted a new question on 2024-02-13T22:10:58Z: Proving that equality is decidable on an Inductive Set – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 17 2024 at 16:23):

Ian Maxwell posted a new question on 2024-02-17T16:15:11Z: Defining and using bisimilarity for negatively-defined conatural numbers – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 17 2024 at 23:53):

Deedit posted a new question on 2024-02-17T23:44:38Z: Decider for lists In Fixpoint – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 18 2024 at 19:36):

Pablo Martín Viñuelas posted a new question on 2024-02-18T19:33:45Z: Unable to install Coq-Polyhedra – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 19 2024 at 08:38):

user23439360 posted a new question on 2024-02-19T08:31:27Z: Multiple Assignements in a Coq Map to the same value – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 22 2024 at 12:15):

andreas posted a new question on 2024-02-22T11:58:36Z: The specialize tatic in Coq does not work well with typeclasses? – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 22 2024 at 18:27):

Dave posted a new question on 2024-02-22T18:21:42Z: Stuck in a proof about sum types and nonempty lists – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 23 2024 at 05:57):

Soundwave posted a new question on 2024-02-23T05:43:41Z: Coq - Overloading over multiple parameters with canonical structures – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 25 2024 at 17:11):

LightQuantum posted a new question on 2024-02-25T17:01:46Z: Induction on indexed type family without JMeq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Feb 25 2024 at 19:20):

someStudentCS posted a new question on 2024-02-25T19:12:23Z: Coq Decreasing Argument mapping – stackoverflow.com

view this post on Zulip StackExchange Bot (Feb 27 2024 at 14:55):

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

view this post on Zulip StackExchange Bot (Feb 28 2024 at 12:42):

Ulises Torrella posted a new question on 2024-02-28T12:39:10Z: Coq can't define an inductive proposition – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 04 2024 at 14:58):

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

view this post on Zulip StackExchange Bot (Mar 12 2024 at 21:41):

ayylien posted a new question on 2024-03-12T21:33:39Z: Split multiple conjuncts in the goal – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 13 2024 at 00:55):

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

view this post on Zulip StackExchange Bot (Mar 14 2024 at 11:25):

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

view this post on Zulip StackExchange Bot (Mar 15 2024 at 16:16):

Charles Averill posted a new question on 2024-03-15T16:12:14Z: Proving non-existence of "least" subtype generator in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 16 2024 at 12:16):

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

view this post on Zulip StackExchange Bot (Mar 18 2024 at 01:44):

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

view this post on Zulip StackExchange Bot (Mar 19 2024 at 04:36):

ayylien posted a new question on 2024-03-19T04:22:54Z: Understanding nat_ind2 in Logical Foundations – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 19 2024 at 13:30):

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

view this post on Zulip StackExchange Bot (Mar 20 2024 at 15:03):

user6584 posted a new question on 2024-03-20T14:56:32Z: Syntax of the case tactic in coq – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 21 2024 at 03:42):

user2628206 posted a new question on 2024-03-21T03:28:56Z: Assistance using destruct on an equality proof for functors – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 21 2024 at 18:55):

user6584 posted a new question on 2024-03-21T18:52:04Z: Showing polynomial equality in coq/ssreflect – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 22 2024 at 22:54):

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

view this post on Zulip StackExchange Bot (Mar 23 2024 at 12:13):

mindconnect.cc posted a new question on 2024-03-23T12:08:09Z: How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)? – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 23 2024 at 22:37):

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

view this post on Zulip StackExchange Bot (Mar 26 2024 at 11:30):

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

view this post on Zulip StackExchange Bot (Mar 27 2024 at 11:55):

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

view this post on Zulip StackExchange Bot (Mar 27 2024 at 22:11):

Kevin Chen posted a new question on 2024-03-27T22:06:22Z: write a coq code to proof constant not surjective – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 28 2024 at 19:16):

Agnishom Chattopadhyay posted a new question on 2024-03-28T19:07:48Z: Tactic to Propify a bool expression – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Mar 29 2024 at 10:58):

Natasha Klaus posted a new question on 2024-03-29T10:48:25Z: Coq : mutually recursive definitions with [mrec] in InteractionTrees Library – stackoverflow.com

view this post on Zulip StackExchange Bot (Mar 29 2024 at 19:46):

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

view this post on Zulip StackExchange Bot (Apr 02 2024 at 21:08):

RataMágica posted a new question on 2024-04-02T21:04:30Z: what symbols can I use in coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 05 2024 at 17:07):

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

view this post on Zulip StackExchange Bot (Apr 06 2024 at 01:46):

user2628206 posted a new question on 2024-04-06T01:44:44Z: Packaging Mathematical Structures in Coq: Help Understanding a Definition – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 07 2024 at 00:18):

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

view this post on Zulip StackExchange Bot (Apr 07 2024 at 16:28):

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

view this post on Zulip StackExchange Bot (Apr 08 2024 at 10:46):

Pietro Braione posted a new question on 2024-04-08T10:33:12Z: How do I express a negative premise in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 12 2024 at 13:05):

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

view this post on Zulip StackExchange Bot (Apr 13 2024 at 19:33):

udduu posted a new question on 2024-04-13T19:21:32Z: Is is possible to rename a coq term? – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 14 2024 at 18:31):

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

view this post on Zulip StackExchange Bot (Apr 15 2024 at 07:50):

ignorant student posted a new question on 2024-04-15T07:48:03Z: Dealing an equality with coq. - beginner's question – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 16 2024 at 02:43):

Siam posted a new question on 2024-04-16T02:21:30Z: Proof for Question V.10 – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 16 2024 at 19:42):

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

view this post on Zulip StackExchange Bot (Apr 16 2024 at 20:58):

Agnishom Chattopadhyay posted a new question on 2024-04-16T20:53:02Z: How do I enable this kind of rewriting? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 17 2024 at 13:50):

camsterwheel posted a new question on 2024-04-17T13:45:44Z: Trouble proving a theorem using induction – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 17 2024 at 14:51):

camsterwheel posted a new question on 2024-04-17T13:45:44Z: Trouble proving a theorem using induction in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 18 2024 at 05:49):

scubed posted a new question on 2024-04-18T05:37:40Z: Inductive from CoInductive? – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 18 2024 at 17:22):

RudeOnion posted a new question on 2024-04-18T17:00:42Z: Struggling with the three_and_five theorem – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 19 2024 at 05:57):

scubed posted a new question on 2024-04-19T05:55:26Z: Inductive from CoInductive? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 23 2024 at 09:33):

radrow posted a new question on 2024-04-23T09:17:18Z: How to instruct auto to simplify the goal during proof search? – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 23 2024 at 22:11):

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

view this post on Zulip StackExchange Bot (Apr 24 2024 at 21:46):

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

view this post on Zulip StackExchange Bot (Apr 26 2024 at 12:35):

Natasha Klaus posted a new question on 2024-04-26T12:22:46Z: InteractionTrees library - simple program on ASM – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 26 2024 at 23:14):

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

view this post on Zulip StackExchange Bot (Apr 27 2024 at 15:11):

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

view this post on Zulip StackExchange Bot (Apr 28 2024 at 18:20):

Jay Lee posted a new question on 2024-04-28T18:10:54Z: What does induction ... in ... do in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Apr 28 2024 at 20:18):

Doktor Diagoras posted a new question on 2024-04-28T20:08:18Z: Eliminating impossible branches in Coq dependent pattern matching – stackoverflow.com

view this post on Zulip StackExchange Bot (Apr 29 2024 at 09:24):

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

view this post on Zulip StackExchange Bot (Apr 30 2024 at 21:49):

Agnishom Chattopadhyay posted a new question on 2024-04-30T21:45:21Z: Rewriting/Applying unidirectional morphisms in Coq – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (May 02 2024 at 09:18):

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

view this post on Zulip StackExchange Bot (May 02 2024 at 18:26):

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

view this post on Zulip StackExchange Bot (May 04 2024 at 02:35):

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

view this post on Zulip StackExchange Bot (May 06 2024 at 03:48):

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

view this post on Zulip StackExchange Bot (May 08 2024 at 10:59):

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

view this post on Zulip StackExchange Bot (May 10 2024 at 09:15):

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

view this post on Zulip StackExchange Bot (May 13 2024 at 08:29):

FH35 posted a new question on 2024-05-13T08:19:58Z: Lemma about a graph in Coq – stackoverflow.com

view this post on Zulip StackExchange Bot (May 13 2024 at 17:33):

radrow posted a new question on 2024-05-13T17:21:27Z: How to mix sections with hints in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (May 15 2024 at 03:42):

Cs_J posted a new question on 2024-05-15T03:33:59Z: Defining mutually recursive types in Coq? – stackoverflow.com

view this post on Zulip StackExchange Bot (May 15 2024 at 15:15):

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

view this post on Zulip StackExchange Bot (May 15 2024 at 23:05):

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

view this post on Zulip StackExchange Bot (May 16 2024 at 10:55):

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