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 Michael Soegtrop (Jun 23 2022 at 14:52):

I can't quite follow this argument. It is quite easy to find such an n constructively - just one can't find the smallest n which is larger than x. One can compute constructively any real number to arbitrary precision. Let's take precision 1 and compute our Cauchy series for x to precision 1. This results in a rational number x' for which we know that |x-x'|<=1. The rationals are Archimedian, so we can compute a n>x'+1>=x. Where is the issue?

view this post on Zulip James Wood (Jun 23 2022 at 15:04):

@Michael Soegtrop Wrong thread

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 04:44):

with-forest posted a new question on July 12, 2022 at 06:07AM: How to prove "$x \le y$" or "not $(x \le y)$" for rational numbers $x$ and $y$ in Coq? – proofassistants.stackexchange.com

view this post on Zulip StackExchange Bot (Jul 12 2022 at 06:44):

with-forest posted a new question on July 12, 2022 at 06:07AM: How to prove "$x \le y$" or "$y < x$" for rational numbers $x$ and $y$ 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 MMY MMY (Jul 24 2022 at 07:45):

How can I represent this set union in Coq?
Domain.png

view this post on Zulip James Wood (Jul 24 2022 at 08:53):

Yeah, I suppose ∪ with a dot over it represents a disjoint union, and cases of an Inductive (or Variant) give you basically that.

view this post on Zulip James Wood (Jul 24 2022 at 08:53):

(This should be in a different thread, by the way.)

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 jay bee (Nov 08 2022 at 17:48):

Hello all,

I am using VSCoq for coq. It has worked up until now, however now when I try to step through my Coq, VSCode gives error output (pasted below). I'm not totally sure what to do about this -- if it's a brew issue, I ran brew update and brew doctor and still nothing. I even reinstalled coq.

Here's my error output:
coqtop started with pid 39914
Client connected on main channel R (port 59734)
Client connected on main channel W (port 59735)
Client connected on control channel R (port 59736)
Client connected on control channel W (port 59737)


Call Init()
coqtop-stderr: Error:
Anomaly
"Uncaught exception Failure("Config file not found - neither /opt/homebrew/etc/findlib.conf nor the directory /opt/homebrew/etc/findlib.conf.d")."
Please report at http://coq.inria.fr/bugs/.

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


Last updated: Feb 01 2023 at 11:04 UTC