1. Can any one help me how to prove this theorem in Coq
2. Can you prove Excluded Middle is wrong in Coq if I do not import classical logic
3. Characteristic function of a union
4. Classical axioms implies every proposition is decidable?
5. Coq: Prop versus Set in Type(n)
6. Decidable equality statement with Set vs. Prop
7. Decide disjunctions in sort Prop
8. Difference between sumbool and intuitionnistic disjunction
9. even_Sn_not_even_n - apply 1 hypothesis in another
10. How to enumerate set in Coq Ensemble
11. How to extract the witness from exists in Coq in function notation/without destructing?
12. Lift existentials in Coq
13. Pigeonhole proof without decidable equality or excluded middle
14. Proof by contradiction in Coq
15. Proving a property on sets
16. Stronger completeness axiom for real numbers in Coq
17. What is a concrete example of the type Set and what is the meaning of Set?
18. Why are logical connectives and booleans separate in Coq?
19. Why not have Prop : Set in Coq?

1. Best way to handle (sub) types of the form { x : nat | x >= 13 /x <= 19 }?
2. Coq - Coercion of list nat
3. Coq: coercion/subtyping between complex expressions
4. Coq coercions and goal matching
5. Coq notation for multi type list
6. Coq - return value of type which is equal to function return type
7. Defining subtype relation in Coq
8. Fixpoint with Prop inhabitant as argument
9. How could I make example for sigma type in Coq?
10. How to convert propositional formula to DNF in Coq
11. In Coq, How to construct an element of 'sig' type
12. make subset types compatible for function application
13. Record equality in Coq
14. Subset parameter
15. Which vector library to use in Coq?

1. Coq: How to refer to the types generated by a specific constructor?
2. Coq QArith division by zero is zero, why?
3. How to prove equality from equality of Some
4. Non-positive occurrence due to polymorphic function
5. Proof leaking in Coq extraction?
6. Proofs of structural properties of arguments in match in coq
7. Recursive partial functions in Coq
8. Using dependent types in Coq (safe nth function)
9. Using induction starting from 1 in Coq
10. Wellfounded induction in Coq

1. Call a theorem using let-in
2. Compute if in a decideable prop in Coq
3. Compute with a recursive function defined by well-defined induction
4. Coq can't compute a well-founded function on Z, but it works on nat
5. Coq identity term which is not eq_refl
6. Coq item 1.2.10 Type cast
7. Coq: unfolding class instances
8. Deriving facts on pattern matching in Coq
9. Error in defining Ackermann in Coq
10. Eval compute is incomplete when own decidability is used in Coq
11. Explain a simple operation in Coq
12. How can I automate counting within proofs in Coq?
13. How can I avoid stack overflow or segmentation fault in Coq nats?
14. How does decidable equality works with List.remove?
15. How proof functions prove?
16. How to define set in Coq without defining set as a list of elements
17. How to extract the witness from exists in Coq in function notation/without destructing?
18. How to make sublists in Coq?
19. How to optimize a search in Coq
20. How to prove decidability of a partial order inductive predicate?
21. How to prove that a number is prime using Znumtheory in Coq
22. I need help defining a concatenation in Coq
23. Incorrect elimination of X in the inductive type or
24. Problems with dependent types in Coq proof assistant
25. Proof leaking in Coq extraction?
26. Prove equality on Sigma-types
27. Proving decidability for a datatype that includes a vector
28. Reasoning about typeclass instance that has been picked up in a theorem?
29. Rewrite single occurence in Ltac
30. rewrite works for = but not for <-> (iff) in Coq
31. Some help dealing with inject/unject and vector types
32. Specialization of module argument in Coq
33. Structural recursion on two arguments
34. Tactic automation: simple decision procedure
35. Transform casual list into dependently typed list in Coq
36. Typeclasses with multiple fields vs. single field in Coq / Unexpected behaviour of Compute command
37. Under what conditions does Eval cbv delta in expand a definition in Coq?
38. Understanding how pattern matching works in Coq
39. Why are logical connectives and booleans separate in Coq?
40. Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?

1. About the refine tactic in Coq
2. Apply rewrite tactic to sub-expression
3. Coq: automate repeated rewriting
4. Coq: destruct (co)inductive hypothesis without losing information
5. How to prove equality from equality of Some
6. How to prove False from obviously contradictory assumptions
7. How to provide proof that two values are different?
8. Inductive definition for family of types
9. Inverting an obviously untrue hypothesis does not prove falsehood
10. Proof automation in Coq how to factorize a proof
11. Proving False with negative inductive types in Coq
12. Recursion for Church encoding of equality
13. Removing trivial match clause in Coq
14. Why can I not apply f_equal to a hypothesis?

1. All-quantified type variable in (value) constructor cannot be explicitly typed as wanted
2. Are all proofs of true = true the same?
3. Attempting to use proof irrelevance without creating ill-typed terms
4. Confused about pattern matching in Record constructions in Coq
5. Coq adding a new variable instead of using the correct one
6. Coq: cannot unify inductive types
7. Coq can't infer type parameter in match
8. Coq: How to refer to the types generated by a specific constructor?
9. Coq inference behavior
10. Coq losing information from if-statement when doing recursive function with Program
11. Coq - Obtaining equality from match statement
12. Coq - Rewriting a FMap Within a Relation
13. Defining a function that returns one element satisfying the condition
14. Dependent pattern matching
15. Deriving facts on pattern matching in Coq
16. Fixpoint with Prop inhabitant as argument
17. Heterogeneous list in Coq
18. How does one define dependent type with named arguments in Coq without issues in unification in the constructors?
19. How to dependent match on a list with two elements?
20. How to make use of information known about this function type in Coq
21. I need help defining a concatenation in Coq
22. Implementing vector addition in Coq
23. Improving dependently typed reverse function
24. In Coq, How to construct an element of 'sig' type
25. Incorrect elimination of X in the inductive type or
26. Induction over relations
27. Inductive definition for family of types
28. Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
29. Pattern matching using information from theorems
30. Program Fixpoint: recursive call in let and hypothesis of the obligation
31. Proofs of structural properties of arguments in match in coq
32. Prove that the only zero-length vector is nil
33. Recursive partial functions in Coq
34. Removing the last element of a sized list in Coq
35. Renaming part of hypothesis in Coq
36. Retrieving constraints from GADT to ensure exhaustion of pattern matching in Coq
37. Some help dealing with inject/unject and vector types
38. Stuck on a simple proof about regular expressions
39. Using dependent induction tactic to keep information while doing induction
40. Using dependent types in Coq (safe nth function)
41. Vector error: The type of this term is a product
42. Wellfounded induction in Coq
43. Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
44. Why does Coq's typechecker reject my map definition?
45. Why not have Prop : Set in Coq?

1. Abstracting leads to a term ill-typed... yet well-typed
2. Are all proofs of true = true the same?
3. Can any one help me how to prove this theorem in Coq
4. Change a function at one point
5. Characteristic function of a union
6. Classical axioms implies every proposition is decidable?
7. Compute if in a decideable prop in Coq
8. Coq can't compute a well-founded function on Z, but it works on nat
9. Coq: How to prove if statements involving strings?
10. Coq losing information from if-statement when doing recursive function with Program
11. Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
12. Decidable equality statement with Set vs. Prop
13. Decide disjunctions in sort Prop
14. Difference between sumbool and intuitionnistic disjunction
15. Equality in Coq for enumerated types
16. Eval compute is incomplete when own decidability is used in Coq
17. Finding a well founded relation to prove termination of a function that stops decreasing at some point
18. General advice about when to use Prop and when to use bool
19. How can I automate counting within proofs in Coq?
20. How does decidable equality works with List.remove?
21. How to define set in Coq without defining set as a list of elements
22. How to prove decidability of a partial order inductive predicate?
23. How to use an unequality to simplify a if-then-else in Coq?
24. Incorrect elimination of X in the inductive type or
25. Inductively defined dense vector lemmas
26. Inversion produces unexpected existT in Coq
27. Pattern-match on type in order to implement equality for existentially typed constructor in Coq
28. Pattern Matching with Even and Odd Cases
29. Pigeonhole proof without decidable equality or excluded middle
30. Problems with dependent types in Coq proof assistant
31. Proof automation in Coq how to factorize a proof
32. Proof by contradiction in Coq
33. Prove that the only zero-length vector is nil
34. Proving decidability for a datatype that includes a vector
35. Record equality in Coq
36. Stronger completeness axiom for real numbers in Coq
37. Tactic automation: simple decision procedure
38. Using dependent types in Coq (safe nth function)
39. When are the constructors of an inductive type exhaustive?
40. Why haven't newer dependently typed languages adopted SSReflect's approach?

1. Abstracting leads to a term ill-typed... yet well-typed
2. Applying a Program Definition fails with "unable to unify Prop with [goal]"
3. Assert a proposition on multiple witnesses
4. Attempting to use proof irrelevance without creating ill-typed terms
5. Case analysis on evidence of equality type in Coq
6. Coq adding a new variable instead of using the correct one
7. Coq can't infer type parameter in match
8. Coq can't see that two types are the same
9. Coq identity term which is not eq_refl
10. Coq - return value of type which is equal to function return type
11. Deriving facts on pattern matching in Coq
12. Destructing equality of dependent records in Coq
13. Different induction principles for Prop and Type
14. Equality of dependent types and dependent values
15. How do we know all Coq constructors are injective and disjoint?
16. How to provide proof that two values are different?
17. How to use rewrite on a subexpression of the current goal
18. Improving dependently typed reverse function
19. Prove that the only zero-length vector is nil
20. Recursion for Church encoding of equality
21. Removing trivial match clause in Coq
22. Retrieving constraints from GADT to ensure exhaustion of pattern matching in Coq
23. What is Coq's type system doing in this example?
24. What is eq_rect and where is it defined in Coq?
25. When are the constructors of an inductive type exhaustive?
26. Why do Calculus of Construction based languages use Setoids so much?

1. Abstracting patterns in induction rule for inductive predicates for Coq
2. All-quantified type variable in (value) constructor cannot be explicitly typed as wanted
3. Building up tree and decreasing argument of fix
4. Can I tell Coq to do induction from n to n + 2?
5. Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?
6. Cannot determine termination
7. Case analysis on evidence of equality type in Coq
8. Closing a lemma on list of nats
9. Coq: Implementation of split_string and proof that nothing gets deleted
10. Coq induction on modulo
11. Coq: Prop versus Set in Type(n)
12. Coq: Proving relation between < and <=
13. Coq: Proving that the product of n and (S n) is even
14. Coq: Recursive definition of fibonacci is ill-formed
15. Coq theorem proving: Simple fraction law in peano arithmetic
16. Coq: viewing proof term during proof script writing
17. decide equality for Mutually Recursive Types in Coq?
18. Decreasing argument (and what is a Program Fixpoint)
19. Dependent Pair Types
20. Dependent pattern matching
21. Destruct if condition in program fixpoint Coq
22. Error in defining Ackermann in Coq
23. Expanding Recursive Functions In Coq
24. Fixpoint with Prop inhabitant as argument
25. How can I construct terms in first-order logic using Coq?
26. How can I write a function of the following form in Coq?
27. How to convert propositional formula to DNF in Coq
28. How to deal with really large terms generated by Program Fixpoint in Coq?
29. How to define an inductive type and a definition at the same time?
30. How to do induction differently?
31. How to do induction on the length of a list in Coq?
32. How to get an induction principle for nested fix
33. How to make sublists in Coq?
34. How to make use of information known about this function type in Coq
35. How to optimize a search in Coq
36. How to prove that another definition of permutation is the same as the Default Permutation Library for Coq
37. How to prove that terms of a first-order language are well-founded?
38. How to use a custom induction principle in Coq?
39. Induction over relations
40. Induction principle for le
41. Induction proofs on MSets
42. Is it possible to force induction tactic to produce more equations?
43. Lemma about list and rev list
44. Logic: auxilliry lemma for tr_rev_correct
45. mutual recursion on an inductive type and nat
46. Nested recursion and Program Fixpoint or Function
47. Pattern Matching with Even and Odd Cases
48. Problems with dependent types in Coq proof assistant
49. Program Fixpoint: recursive call in let and hypothesis of the obligation
50. Proof by case analysis in Coq
51. Proof leaking in Coq extraction?
52. Proof of the application of a substitution on a term
53. Prove properties of lists
54. Proving decidability for a datatype that includes a vector
55. Proving even + even = even with mutual induction using tactics
56. Proving increasing iota in Coq
57. Proving termination in Coq
58. Proving Termination of Function in Coq
59. Proving that s-expressions printing is injective
60. Proving uniqueness of an instance of an indexed inductive type
61. Reasoning about lists in Coq
62. Recursion for Church encoding of equality
63. Recursive partial functions in Coq
64. Recursive use of typeclass methods in Coq
65. Removing the last element of a sized list in Coq
66. Renaming part of hypothesis in Coq
67. SF Volume 1: Logic: How to prove tr_rev <-> rev?
68. Some help dealing with inject/unject and vector types
69. Structural recursion on two arguments
70. Stuck on a simple proof about regular expressions
71. Stuck on the proof of a simple Lemma: which induction should I use?
72. Teach Coq to check termination
73. Transitivity of subsequence in Coq
74. Turn off automatic induction principle in Coq
75. Understanding "well founded" proofs in Coq
76. Using induction starting from 1 in Coq
77. Using length of list X as an argument for a constructor of X in Coq
78. Using Omega to prove a lemma in Coq
79. Using typeclass instances within typeclasses
80. Vector error: The type of this term is a product
81. Wellfounded induction in Coq
82. What does it mean when Coq expands a function as part of the goal?
83. What is eq_rect and where is it defined in Coq?
84. What's the difference between Program Fixpoint and Function in Coq?
85. Which vector library to use in Coq?
86. Why does Coq's typechecker reject my map definition?
87. Why does nesting the induction tactic also nest the inductive hypotheses under a lambda?
88. Why is my recursive definition of list_min ill-formed?

1. Applying a Program Definition fails with "unable to unify Prop with [goal]"
2. Are all proofs of true = true the same?
3. Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?
4. Case analysis on evidence of equality type in Coq
5. Coq adding a new variable instead of using the correct one
6. Coq: cannot unify inductive types
7. Coq can't see that two types are the same
8. Coq: Proving relation between < and <=
9. Coq QArith division by zero is zero, why?
10. Coq - return value of type which is equal to function return type
11. Decoupling the data to be manipulated from the proofs that the manipulations are justified
12. Destructing equality of dependent records in Coq
13. Difference between type parameters and indices?
14. Different induction principles for Prop and Type
15. Equality on inductive types
16. Function- and Type substitutions or Views in Coq
17. Heterogeneous list in Coq
18. How does one build the list of only true elements in Coq using dependent types?
19. How does one define dependent type with named arguments in Coq without issues in unification in the constructors?
20. How to dependent match on a list with two elements?
21. How to use rewrite on a subexpression of the current goal
22. Implementing vector addition in Coq
23. Improving dependently typed reverse function
24. Induction on predicates with product type arguments
25. Induction over relations
26. Inductive definition for family of types
27. Inductively defined dense vector lemmas
28. Inversion produces unexpected existT in Coq
29. Is it possible to force induction tactic to produce more equations?
30. mutual recursion on an inductive type and nat
31. Non-positive occurrence due to polymorphic function
32. Prove that the only zero-length vector is nil
33. Proving decidability for a datatype that includes a vector
34. Proving uniqueness of an instance of an indexed inductive type
35. Removing the last element of a sized list in Coq
36. Representing Higher-Order Functors as Containers in Coq
37. Retrieving constraints from GADT to ensure exhaustion of pattern matching in Coq
38. Understanding specialize tactic
39. Understanding the intros keyword work in Coq
40. Using dependent types in Coq (safe nth function)
41. Using length of list X as an argument for a constructor of X in Coq
42. Vector error: The type of this term is a product
43. What is Coq's type system doing in this example?
44. When are the constructors of an inductive type exhaustive?
45. Why can't Coq infer the that 0 + n = n in this dependently typed program?
46. Why does Coq's typechecker reject my map definition?
47. Why haven't newer dependently typed languages adopted SSReflect's approach?

1. Are all proofs of true = true the same?
2. Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?
3. Case analysis on evidence of equality type in Coq
4. context expression in Coq
5. Coq auto tactic fails
6. Coq identity term which is not eq_refl
7. Coq losing information from if-statement when doing recursive function with Program
8. Coq: Recursive definition of fibonacci is ill-formed
9. Dealing with let-in expressions in current goal
10. Equality in Coq for enumerated types
11. Equality on inductive types
12. Explain a simple operation in Coq
13. Fail to use let-destruct for tuple in Coq
14. Finding a well founded relation to prove termination of a function that stops decreasing at some point
15. How can I use type arguments in an ltac?
16. How do you lookup the definition or implementation of Coq proof tactics?
17. How does one build the list of only true elements in Coq using dependent types?
18. How to debug tactic failure in a match goal branch?
19. How to "extract" Z from subset type {z : Z | z > 0}
20. How to match a match expression?
21. In Coq, "if then else" allows non-boolean first argument?
22. Induction on predicates with product type arguments
23. Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
24. Ltac pattern matching: why does forall x, ?P x not match forall x, x?
25. Matching expression context under forall with Ltac
26. Pattern-match on type in order to implement equality for existentially typed constructor in Coq
27. Proofs about constructors matched with _
28. Prove that the only zero-length vector is nil
29. Recursive partial functions in Coq
30. Redundant clause in match
31. Retrieving constraints from GADT to ensure exhaustion of pattern matching in Coq
32. Shorter notation for matching hypotheses in Coq?
33. Transform casual list into dependently typed list in Coq
34. Understanding how pattern matching works in Coq
35. What is Coq's type system doing in this example?
36. Why can't Coq infer the that 0 + n = n in this dependently typed program?
37. Why does Coq's typechecker reject my map definition?
38. Why does this Coq Definition fail? Coq Namespace error for Inductive Type
39. Why does use of Coq's setoid_replace ... by clause need an extra idtac?
40. Why is my recursive definition of list_min ill-formed?

1. Best practices for parametrized Coq libraries
2. Coq: Derive argument from context
3. Coq: local ltac definition
4. Display the original name of the imported module in Coq
5. Efficient Way of Defining Multiple Functions of the Same Type
6. How do you make notations visible outside of a module signature in Coq?
7. How to add variables introduced by set tactic to a Hint DB?
8. How to deal with really large terms generated by Program Fixpoint in Coq?
9. How to do induction on the length of a list in Coq?
10. How to import the library Coq.Arith.PeanoNat in Coq?
11. How to set defaults for implicit arguments when they can't be inferred?
12. How to use a custom induction principle in Coq?
13. How to use modules to hide lemmas in Coq?
14. How to use the Lemma inside a module in Coq?
15. Import vs. Include in Coq Module system
16. Local Inductive definitions and Theorems
17. Proving decidability for a datatype that includes a vector
18. Require, Import, Require Import
19. Section mechanism in Coq. Forbid omitting of hypotheses from context
20. Specialization of module argument in Coq
21. Stuck on a simple proof about regular expressions
22. Type encapsulation in Coq
23. Use module signature definition in module implementation
24. Using Implicit Type Class Parameters in Coq Notation
25. Using local notation inside a Coq theorem

1. Building up tree and decreasing argument of fix
2. Coq produce instance of a type {x : T | P x} inside an explicit definition given an x of type T
3. Error in defining Ackermann in Coq
4. Explain a simple operation in Coq
5. Fail to use let-destruct for tuple in Coq
6. Heterogeneous list in Coq
7. How to convert propositional formula to DNF in Coq
8. How to deal with really large terms generated by Program Fixpoint in Coq?
9. How to define an inductive type and a definition at the same time?
10. How to dependent match on a list with two elements?
11. How to get an induction principle for nested fix
12. How to make use of information known about this function type in Coq
13. How to match a match expression?
14. How to prove that terms of a first-order language are well-founded?
15. Implementing vector addition in Coq
16. mutual recursion on an inductive type and nat
17. Problems with dependent types in Coq proof assistant
18. Proof of the application of a substitution on a term
19. Proving termination in Coq
20. Proving Termination of Function in Coq
21. Proving that s-expressions printing is injective
22. Teach Coq to check termination
23. Using Implicit Type Class Parameters in Coq Notation
24. Using length of list X as an argument for a constructor of X in Coq
25. Using typeclass instances within typeclasses
26. Vector error: The type of this term is a product
27. What's the difference between Program Fixpoint and Function in Coq?
28. Why is my recursive definition of list_min ill-formed?

1. Call a theorem using let-in
2. Coq losing information from if-statement when doing recursive function with Program
3. Definition vs Notation for constants
4. Dependent pattern matching
5. How can I avoid stack overflow or segmentation fault in Coq nats?
6. How to define an automatically unfoldable definition
7. How to disable my custom notation in Coq?
8. Interaction between type classes and auto tactic
9. Is it possible to declare type-dependent Notation in Coq?
10. Ltac: optional arguments tactic
11. Multiple where-clauses for Reserved Notation in Coq?
12. Syntax error with < in Coq notations
13. Trouble writing my notation for natural numbers in Coq
14. Unfold a notation within a scope
15. Unfold notation in ltac
16. Using Implicit Type Class Parameters in Coq Notation
17. Why does Coq.Init.Logic define the notation A -> B?

1. A Coq proof of a theorem which turns a formula containing y into a formula containing f(x)
2. Can you prove Excluded Middle is wrong in Coq if I do not import classical logic
3. Coq can't compute a well-founded function on Z, but it works on nat
4. Coq Index Relation
5. Coq: Prop versus Set in Type(n)
6. Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
7. Definition by property in Coq
8. Difference between parameters and members of a class
9. Difference between sumbool and intuitionnistic disjunction
10. Different induction principles for Prop and Type
11. Incorrect elimination of X in the inductive type or
12. Inductively defined dense vector lemmas
13. Lift existentials in Coq
14. Non-positive occurrence due to polymorphic function
15. Proof leaking in Coq extraction?
16. Prove equality on Sigma-types
17. Record equality in Coq
18. Subtyping in Coq
19. Why can't Coq infer the that 0 + n = n in this dependently typed program?
20. Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
21. Why haven't newer dependently typed languages adopted SSReflect's approach?
22. Why not have Prop : Set in Coq?

1. Agda-like programming in Coq/Proof General?
2. All-quantified type variable in (value) constructor cannot be explicitly typed as wanted
3. Assert a proposition on multiple witnesses
4. Compute if in a decideable prop in Coq
5. Compute with a recursive function defined by well-defined induction
6. Contradiction on natural number's zero test
7. Coq can't see that two types are the same
8. Coq: easiest way to construct members of a decidable sigma type?
9. Coq execution difference between semicolon ; and period .
10. Coq: How to prove if statements involving strings?
11. Coq: How to prove max a b <= a + b?
12. Coq: How to refer to the types generated by a specific constructor?
13. Coq inference behavior
14. Coq leb (<=?) does not give me an hypothesis after case or induction
15. Coq produce instance of a type {x : T | P x} inside an explicit definition given an x of type T
16. Coq proving addition inequality
17. Coq: Proving that the product of n and (S n) is even
18. Coq QArith division by zero is zero, why?
19. Coq Qed raise a warning with admitted lemmas
20. Coq - return value of type which is equal to function return type
21. Coq - Rewriting a FMap Within a Relation
22. Coq: viewing proof term during proof script writing
23. Decoupling the data to be manipulated from the proofs that the manipulations are justified
24. Definition by property in Coq
25. Deriving facts on pattern matching in Coq
26. Does Gallina have holes like in Agda?
27. Ease life in dependently typed programming using Function and Program in Coq
28. Eliminate redundant sub-goals generated by case analysis in Coq
29. Eval compute is incomplete when own decidability is used in Coq
30. even_Sn_not_even_n - apply 1 hypothesis in another
31. Existential quantifier in Coq impredicative logic (System F)
32. Expanding Recursive Functions In Coq
33. Extensible tactic in Coq
34. Finding a well founded relation to prove termination of a function that stops decreasing at some point
35. Fixpoint with Prop inhabitant as argument
36. Function- and Type substitutions or Views in Coq
37. General advice about when to use Prop and when to use bool
38. How can I avoid stack overflow or segmentation fault in Coq nats?
39. How can I implement a Coq tactic that iterates over the hypotheses?
40. How do I change a concrete variable to an existentially quantified var in a hypothesis?
41. How does decidable equality works with List.remove?
42. How to add to both sides of an equality in Coq
43. How to apply a function once during simplification in Coq?
44. How to do cases with an inductive type in Coq
45. How to extract the witness from exists in Coq in function notation/without destructing?
46. How to give a counterxample in Coq?
47. How to implement a union-find (disjoint set) data structure in Coq?
48. How to improve this proof?
49. How to leave a goal unfinished in Coq
50. How to make algebraic manipulations in Coq easier?
51. How to make use of information known about this function type in Coq
52. How to prove that terms of a first-order language are well-founded?
53. How to repeat proof tactics in case in Coq?
54. How to replace a term with some property of the term?
55. How to unfold a recursive function just once in Coq
56. How to use an unequality to simplify a if-then-else in Coq?
57. How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 by auto but in Coq?
58. Idiomatic ways of selecting subterm to rewrite
59. In Coq, is there a way to see the tactics applied by tauto?
60. Instantiating an existential with a specific proof
61. Interactive theorem proving with no specified goal
62. Just a universally quantified hypotesis in Coq proof
63. Merge duplicate cases in match Coq
64. Nested recursion and Program Fixpoint or Function
65. Pattern matching using information from theorems
66. Pigeonhole proof without decidable equality or excluded middle
67. Port a Coq lemma over Z to a similar lemma over nat
68. Pose proof in Coq
69. Proof automation in Coq how to factorize a proof
70. Proof by case analysis in Coq
71. Proving a property on sets
72. Proving False with negative inductive types in Coq
73. Rewriting hypothesis to false with a contradictory theorem
74. Show theorem definition in Coq
75. Some help dealing with inject/unject and vector types
76. Stuck on a simple proof about regular expressions
77. Stuck on the proof of a simple Lemma: which induction should I use?
78. Transitivity of -> in Coq
79. Using dependent types in Coq (safe nth function)
80. Vector error: The type of this term is a product
81. Wellfounded induction in Coq
82. What is the difference between Lemma and Theorem in Coq
83. Why does nesting the induction tactic also nest the inductive hypotheses under a lambda?
84. Why is my recursive definition of list_min ill-formed?

1. Call a theorem using let-in
2. Coq - return value of type which is equal to function return type
3. Coq: Testing partial convertibilty
4. Coq: typeclasses vs dependent records
5. Defining subtype relation in Coq
6. Existential goals are filled in too soon
7. I need help defining a concatenation in Coq
8. Lemma as a type in a record
9. Record and Definition
10. Recursive use of typeclass methods in Coq
11. Returning a record from a definition in Coq
12. Type encapsulation in Coq
13. Why haven't newer dependently typed languages adopted SSReflect's approach?

1. Can I tell Coq to do induction from n to n + 2?
2. Contradiction on natural number's zero test
3. Coq leb (<=?) does not give me an hypothesis after case or induction
4. Eval compute is incomplete when own decidability is used in Coq
5. even_Sn_not_even_n - apply 1 hypothesis in another
6. General advice about when to use Prop and when to use bool
7. How can I automate counting within proofs in Coq?
8. How can I prove that she cannot prove Or_commutative with only intro and apply?
9. How does decidable equality works with List.remove?
10. How to convert propositional formula to DNF in Coq
11. How to define set in Coq without defining set as a list of elements
12. How to extract the witness from exists in Coq in function notation/without destructing?
13. How to implement a union-find (disjoint set) data structure in Coq?
14. How to prove that a number is prime using Znumtheory in Coq
15. I need help defining a concatenation in Coq
16. Lemma as a type in a record
17. Pattern-match on type in order to implement equality for existentially typed constructor in Coq
18. Pigeonhole proof without decidable equality or excluded middle
19. Port a Coq lemma over Z to a similar lemma over nat
20. Problems with dependent types in Coq proof assistant
21. Proof automation in Coq how to factorize a proof
22. Prove a constant is even
23. Proving equivalence of two programs expressed as different types
24. Record equality in Coq
25. Transitivity of -> in Coq
26. Using dependent types in Coq (safe nth function)
27. Why does this Coq Definition fail? Coq Namespace error for Inductive Type
28. Why haven't newer dependently typed languages adopted SSReflect's approach?
29. Why S n' =? S n' simplifies to n' =? n' in Coq?

1. A Coq proof of a theorem which turns a formula containing y into a formula containing f(x)
2. Assert a proposition on multiple witnesses
3. Best way to handle (sub) types of the form { x : nat | x >= 13 /x <= 19 }?
4. Coq: easiest way to construct members of a decidable sigma type?
5. Coq Index Relation
6. Coq produce instance of a type {x : T | P x} inside an explicit definition given an x of type T
7. Definition by property in Coq
8. Dependent Pair Types
9. Dependent pattern matching
10. Dependent type as a function argument in Coq
11. Destructing equality of dependent records in Coq
12. Difference between parameters and members of a class
13. How can I read Coq's definition of proj1_sig?
14. How do I change a concrete variable to an existentially quantified var in a hypothesis?
15. How to extract the witness from exists in Coq in function notation/without destructing?
16. How to "extract" Z from subset type {z : Z | z > 0}
17. How to name the assumption when remembering an expression?
18. I need help defining a concatenation in Coq
19. In Coq, How to construct an element of 'sig' type
20. Inductively defined dense vector lemmas
21. make subset types compatible for function application
22. Non-positive occurrence due to polymorphic function
23. Pattern matching using information from theorems
24. Proofs of structural properties of arguments in match in coq
25. Prove equality on Sigma-types
26. Proving Termination of Function in Coq
27. Recursive partial functions in Coq
28. Relation between types prod and sig in Coq
29. Subset parameter
30. Using dependent types in Coq (safe nth function)
31. Which vector library to use in Coq?
32. Why can't Coq infer the that 0 + n = n in this dependently typed program?

1. Coq: a single notation for multiple constructors
2. Coq: Testing partial convertibilty
3. Eliminate redundant sub-goals generated by case analysis in Coq
4. Equality in Coq for enumerated types
5. How to dependent match on a list with two elements?
6. Instantiating an existential with a specific proof
7. Proofs about constructors matched with _
8. Proofs of structural properties of arguments in match in coq

1. About the refine tactic in Coq
2. All-quantified type variable in (value) constructor cannot be explicitly typed as wanted
3. Apply rewrite tactic to sub-expression
4. Applying a Program Definition fails with "unable to unify Prop with [goal]"
5. Attempting to use proof irrelevance without creating ill-typed terms
6. Best practices for an effective use of Coq's hint database
7. Can Coq intros pattern split at the rightmost opportunity for conjunction?
8. Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?
9. Cannot rewrite goal with assertion?
10. Can't automate a lemma that works manually in Coq
11. Compute with a recursive function defined by well-defined induction
12. Coq: a left-recursive notation must have an explicit level
13. Coq: adding a "strong induction" tactic
14. Coq - Assign expression to variable
15. Coq auto tactic fails
16. Coq: automate repeated rewriting
17. Coq can't see that two types are the same
18. Coq: controlling subst when we have many equalities
19. Coq: destruct (co)inductive hypothesis without losing information
20. Coq execution difference between semicolon ; and period .
21. Coq: How are the equality tactics symmetry and transitivity defined?
22. Coq induction on modulo
23. Coq inference behavior
24. Coq produce instance of a type {x : T | P x} inside an explicit definition given an x of type T
25. Coq Qed raise a warning with admitted lemmas
26. Coq: rewrite preserving input hypothesis
27. Coq rewriting using lambda arguments
28. Coq: Rewriting with forall in hypothesis or goal
29. Coq theorem proving: Simple fraction law in peano arithmetic
30. Coq: viewing proof term during proof script writing
31. Creating Coq tactic: how to use a newly generated name?
32. Definition vs Notation for constants
33. Eliminate redundant sub-goals generated by case analysis in Coq
34. Equality in Coq for enumerated types
35. Equality on inductive types
36. Error in defining Ackermann in Coq
37. Error "Tactic failure: The relation (fun x y : BloodType => x <> y) is not a declared reflexive relation." when proving a theorem about function
38. Existential goals are filled in too soon
39. Existential instantiation and generalization in coq
40. Existential quantifier in Coq impredicative logic (System F)
41. Expanding Recursive Functions In Coq
42. Explain a simple operation in Coq
43. Explanation transitivity of equal Coq
44. Extensible tactic in Coq
45. Form of intros in Coq specifically for forall and explicitly for ->
46. Generalising a set of proofs in Coq
47. Generalizing existential variables in Coq
48. Generalizing expressions under binders
49. Generic equality lifting in Coq
50. Hint Rewrite cannot infer parameter
51. How can I automate counting within proofs in Coq?
52. How can I generalise Coq proofs of an iff?
53. How can I implement a Coq tactic that iterates over the hypotheses?
54. How can I read Coq's definition of proj1_sig?
55. How can I rewrite selectively in Coq?
56. How can I use type arguments in an ltac?
57. How could I make example for sigma type in Coq?
58. How do I change a concrete variable to an existentially quantified var in a hypothesis?
59. How do I provide implicit arguments explicitly in Coq?
60. How do we know all Coq constructors are injective and disjoint?
61. How do you lookup the definition or implementation of Coq proof tactics?
62. How do you selectively simplify arguments to each time a function is called, without evaluating the function itself?
63. How does auto interract with biconditional (iff)
64. How does one inspect what more complicated tactics do in Coq step-by-step?
65. How to add "assumed true" statements in Coq
66. How to add to both sides of an equality in Coq
67. How to apply a function once during simplification in Coq?
68. How to debug tactic failure in a match goal branch?
69. How to define an automatically unfoldable definition
70. How to define axiom of a line as two points in Coq
71. How to destruct pair equivalence in Coq?
72. How to do cases with an inductive type in Coq
73. How to do "negative" match in Ltac?
74. How to forbid simpl tactic to unfold arithmetic expressions?
75. How to import libraries in Coq?
76. How to improve this proof?
77. How to introduce a new existential condition from a witness in Coq?
78. How to introduce a new variable in Coq?
79. How to leave a goal unfinished in Coq
80. How to leverage auto's searching and hint databases in custom tactics?
81. How to make algebraic manipulations in Coq easier?
82. How to name the assumption when remembering an expression?
83. How to prove decidability of a partial order inductive predicate?
84. How to prove equality from equality of Some
85. How to prove False from obviously contradictory assumptions
86. How to prove non-equality of terms produced by two different constructors of the same inductive in Coq?
87. How to provide proof that two values are different?
88. How to repeat proof tactics in case in Coq?
89. How to replace a term with some property of the term?
90. How to return a (intro'd) hypothesis back to the goal formula?
91. How to save the current goal/subgoal as an assert lemma
92. How to solve contradiction in Coq
93. How to specialize nested hypotheses in Coq?
94. How to specify explicit equality in Coq search patterns?
95. How to step through semicolons separated tactics sequence in coqide?
96. How to systematically normalize inequalities to < (lt) and <= (le) in Coq?
97. How to turn an single unification variable into a goal, during proof
98. How to unfold a recursive function just once in Coq
99. How to use auto with repeat in custom tactics?
100. How to use rewrite on a subexpression of the current goal
101. How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 by auto but in Coq?
102. Idiomatic ways of selecting subterm to rewrite
103. In Coq, How to construct an element of 'sig' type
104. In Coq, how to remove a defined variable from the namespace?
105. In Coq: inversion of existential quantifier with multiple variables, with one command?
106. In Coq, which tactic to change the goal from S x = S y to x = y
107. In-place simplification for Coq
108. In the Coq tactics language, what is the difference between intro and intros
109. Induction on predicates with product type arguments
110. Induction on record member in Coq?
111. Induction over relations
112. Inductive definition for family of types
113. Injectivity of inl and inr in standard library
114. Instantiating an existential with a specific proof
115. Interaction between type classes and auto tactic
116. Inverting an obviously untrue hypothesis does not prove falsehood
117. Is it possible to force induction tactic to produce more equations?
118. Is there a eapply-like tactic that works on exists goals in Coq?
119. Less or equal relation with largest element of natural number list
120. Locating definition of a tactic in Coq proofs
121. Ltac: optional arguments tactic
122. Ltac pattern matching: why does forall x, ?P x not match forall x, x?
123. Matching expression context under forall with Ltac
124. Matching with Ltac on a call containing local variable
125. Multiple successes in Coq branching and backtracking?
126. Nested recursion and Program Fixpoint or Function
127. Pattern-match on type in order to implement equality for existentially typed constructor in Coq
128. Pattern matching using information from theorems
129. Pose proof in Coq
130. Problems with missing information in Obligations when defining using Program in Coq
131. Proof automation in Coq how to factorize a proof
132. Proof automation
133. Proof by case analysis in Coq
134. Proofs about constructors matched with _
135. Proving forall x xs ys, subseq (x :: xs) ys -> subseq xs ys in Coq
136. Proving uniqueness of an instance of an indexed inductive type
137. Question about intros [=] and intros [= <- H]
138. Reasoning about typeclass instance that has been picked up in a theorem?
139. Recursive partial functions in Coq
140. Rewrite single occurence in Ltac
141. Rewrite under exists
142. rewrite works for = but not for <-> (iff) in Coq
143. Shorter notation for matching hypotheses in Coq?
144. Show all axioms Coq
145. Show theorem definition in Coq
146. Some help dealing with inject/unject and vector types
147. Split conjunction goal into subgoals
148. Step by step simplification in Coq?
149. Stuck on a simple proof about regular expressions
150. Stuck on the proof of a simple Lemma: which induction should I use?
151. Subtyping in Coq
152. Tactic automation: simple decision procedure
153. Transferring proof from Z to N in Coq
154. Typeclass resolution and autorewrite
155. Unable to find an instance for the variable
156. Under what conditions does Eval cbv delta in expand a definition in Coq?
157. Understanding specialize tactic
158. Understanding the intros keyword work in Coq
159. Unfold a notation within a scope
160. Unfold notation in ltac
161. Using an existential theorem in Coq
162. Using dependent induction tactic to keep information while doing induction
163. Using local notation inside a Coq theorem
164. Vector : t A n = t A (n+0)?
165. "Verbose" auto in Coq
166. Wellfounded induction in Coq
167. What does it mean when Coq expands a function as part of the goal?
168. What does Proof. simpl. reflexivity. Qed. mean in Coq?
169. What does the tactic destruct do in the proof below?
170. What does the tactic induction followed by a number do?
171. What is difference between destruct and case_eq tactics in Coq?
172. What <> is in Coq
173. What is the difference between Axiom and Variable in Coq
174. What is the difference between Lemma and Theorem in Coq
175. What is the tactic that does nothing?
176. What should be done when simpl does not reduce all the necessary steps?
177. What's the difference between Program Fixpoint and Function in Coq?
178. What's the difference between revert and generalize tactics in Coq?
179. Where did lt_index go?
180. Why can I not apply f_equal to a hypothesis?
181. Why can I use the constructor tactic to prove reflexivity?
182. Why can't I define the following CoFixpoint?
183. Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
184. Why does Coq.Init.Logic define the notation A -> B?
185. Why does use of Coq's setoid_replace ... by clause need an extra idtac?
186. Why is following Coq rewrite not applying on right hand side of assumption?
187. Why S n' =? S n' simplifies to n' =? n' in Coq?
188. Why would the tactic exact be complete for Coq proofs?

1. Best practices for parametrized Coq libraries
2. Building a class hierarchy in Coq?
3. Coq: a single notation for multiple constructors
4. Coq: Derive argument from context
5. Coq: easiest way to construct members of a decidable sigma type?
6. Coq notation for multi type list
7. Coq: typeclasses vs dependent records
8. Coq: usage of PartialOrder typeclass
9. Difference between parameters and members of a class
10. How to set defaults for implicit arguments when they can't be inferred?
11. Interaction between type classes and auto tactic
12. Is it possible to declare type-dependent Notation in Coq?
13. Reasoning about typeclass instance that has been picked up in a theorem?
14. Recursive use of typeclass methods in Coq
15. Tactic automation: simple decision procedure
16. Typeclass resolution and autorewrite
17. Using typeclass instances within typeclasses
18. Why haven't newer dependently typed languages adopted SSReflect's approach?

1. A simple case of universe inconsistency
2. Church numerals and universe inconsistency
3. How to solve goals with invalid type equalities in Coq?
4. Inductive definition of boolean
5. Recursion for Church encoding of equality
6. What is a concrete example of the type Set and what is the meaning of Set?
7. Why not have Prop : Set in Coq?

1. Adding complete disjunctive assumption in Coq
2. Can Coq intros pattern split at the rightmost opportunity for conjunction?
3. Contradiction on natural number's zero test
4. Coq: How to prove if statements involving strings?
5. Coq induction on modulo
6. Coq leb (<=?) does not give me an hypothesis after case or induction
7. Eval compute is incomplete when own decidability is used in Coq
8. even_Sn_not_even_n - apply 1 hypothesis in another
9. How to make sublists in Coq?
10. Merge duplicate cases in match Coq
11. Pattern Matching with Even and Odd Cases
12. Problems with dependent types in Coq proof assistant
13. Using length of list X as an argument for a constructor of X in Coq
14. Why S n' =? S n' simplifies to n' =? n' in Coq?

1. Compute with a recursive function defined by well-defined induction
2. Error in defining Ackermann in Coq
3. How to do induction on the length of a list in Coq?
4. How to prove that terms of a first-order language are well-founded?
5. Proof leaking in Coq extraction?
6. Proving Termination of Function in Coq
7. Recursive partial functions in Coq
8. Structural recursion on two arguments
9. Stuck on the proof of a simple Lemma: which induction should I use?
10. Teach Coq to check termination
11. Understanding "well founded" proofs in Coq

1. Coq: Associativity of relational composition
2. Coq: eliminating forall?
3. Coq path implementation
4. Defining integers inductively in Coq (inductive definitions subject to relations)
5. How do you prove in Coq that (e: p = p) = eq_refl?
6. How proof assistants are implemented?
7. How to write to a file, from Coq

1. A Coq proof of a theorem which turns a formula containing y into a formula containing f(x)
2. A simple case of universe inconsistency
3. About the refine tactic in Coq
4. Abstracting leads to a term ill-typed... yet well-typed
5. Abstracting patterns in induction rule for inductive predicates for Coq
6. Adding complete disjunctive assumption in Coq
7. Agda-like programming in Coq/Proof General?
8. All-quantified type variable in (value) constructor cannot be explicitly typed as wanted
9. Apply rewrite tactic to sub-expression
10. Applying a Program Definition fails with "unable to unify Prop with [goal]"
11. Are all proofs of true = true the same?
12. Assert a proposition on multiple witnesses
13. Attempting to use proof irrelevance without creating ill-typed terms
14. Best practices for an effective use of Coq's hint database
15. Best practices for parametrized Coq libraries
16. Best way to handle (sub) types of the form { x : nat | x >= 13 /x <= 19 }?
17. Building a class hierarchy in Coq?
18. Building up tree and decreasing argument of fix
19. Call a theorem using let-in
20. Can any one help me how to prove this theorem in Coq
21. Can Coq intros pattern split at the rightmost opportunity for conjunction?
22. Can I tell Coq to do induction from n to n + 2?
23. Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?
24. Can you prove Excluded Middle is wrong in Coq if I do not import classical logic
25. Cannot determine termination
26. Cannot rewrite goal with assertion?
27. Can't automate a lemma that works manually in Coq
28. Case analysis on evidence of equality type in Coq
29. Change a function at one point
30. Characteristic function of a union
31. Church numerals and universe inconsistency
32. Classical axioms implies every proposition is decidable?
33. Closing a lemma on list of nats
34. Compute if in a decideable prop in Coq
35. Compute with a recursive function defined by well-defined induction
36. Confused about pattern matching in Record constructions in Coq
37. context expression in Coq
38. Contradiction on natural number's zero test
39. Coq: a left-recursive notation must have an explicit level
40. Coq: a single notation for multiple constructors
41. Coq adding a new variable instead of using the correct one
42. Coq: adding a "strong induction" tactic
43. Coq - Assign expression to variable
44. Coq: Associativity of relational composition
45. Coq auto tactic fails
46. Coq: automate repeated rewriting
47. Coq: cannot unify inductive types
48. Coq can't compute a well-founded function on Z, but it works on nat
49. Coq can't infer type parameter in match
50. Coq can't see that two types are the same
51. Coq - Coercion of list nat
52. Coq: coercion/subtyping between complex expressions
53. Coq coercions and goal matching
54. Coq: controlling subst when we have many equalities
55. Coq: Derive argument from context
56. Coq: destruct (co)inductive hypothesis without losing information
57. Coq: easiest way to construct members of a decidable sigma type?
58. Coq: eliminating forall?
59. Coq execution difference between semicolon ; and period .
60. Coq: How are the equality tactics symmetry and transitivity defined?
61. Coq: How to prove if statements involving strings?
62. Coq: How to prove max a b <= a + b?
63. Coq: How to refer to the types generated by a specific constructor?
64. Coq identity term which is not eq_refl
65. Coq: Implementation of split_string and proof that nothing gets deleted
66. Coq Index Relation
67. Coq induction on modulo
68. Coq inference behavior
69. Coq item 1.2.10 Type cast
70. Coq leb (<=?) does not give me an hypothesis after case or induction
71. Coq: local ltac definition
72. Coq losing information from if-statement when doing recursive function with Program
73. Coq notation for multi type list
74. Coq - Obtaining equality from match statement
75. Coq path implementation
76. Coq produce instance of a type {x : T | P x} inside an explicit definition given an x of type T
77. Coq: Prop versus Set in Type(n)
78. Coq proving addition inequality
79. Coq: Proving relation between < and <=
80. Coq: Proving that the product of n and (S n) is even
81. Coq QArith division by zero is zero, why?
82. Coq Qed raise a warning with admitted lemmas
83. Coq: Recursive definition of fibonacci is ill-formed
84. Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
85. Coq - return value of type which is equal to function return type
86. Coq: rewrite preserving input hypothesis
87. Coq - Rewriting a FMap Within a Relation
88. Coq rewriting using lambda arguments
89. Coq: Rewriting with forall in hypothesis or goal
90. Coq: Testing partial convertibilty
91. Coq theorem proving: Simple fraction law in peano arithmetic
92. Coq: typeclasses vs dependent records
93. Coq: unfolding class instances
94. Coq: usage of PartialOrder typeclass
95. Coq: viewing proof term during proof script writing
96. Creating Coq tactic: how to use a newly generated name?
97. Dealing with let-in expressions in current goal
98. Decidable equality statement with Set vs. Prop
99. Decide disjunctions in sort Prop
100. decide equality for Mutually Recursive Types in Coq?
101. Decoupling the data to be manipulated from the proofs that the manipulations are justified
102. Decreasing argument (and what is a Program Fixpoint)
103. Defining a function that returns one element satisfying the condition
104. Defining integers inductively in Coq (inductive definitions subject to relations)
105. Defining subtype relation in Coq
106. Definition by property in Coq
107. Definition vs Notation for constants
108. Dependent Pair Types
109. Dependent pattern matching
110. Dependent type as a function argument in Coq
111. Deriving facts on pattern matching in Coq
112. Destruct if condition in program fixpoint Coq
113. Destructing equality of dependent records in Coq
114. Difference between parameters and members of a class
115. Difference between sumbool and intuitionnistic disjunction
116. Difference between type parameters and indices?
117. Different induction principles for Prop and Type
118. Display the original name of the imported module in Coq
119. Does Gallina have holes like in Agda?
120. Ease life in dependently typed programming using Function and Program in Coq
121. Efficient Way of Defining Multiple Functions of the Same Type
122. Eliminate redundant sub-goals generated by case analysis in Coq
123. Equality in Coq for enumerated types
124. Equality of dependent types and dependent values
125. Equality on inductive types
126. Error in defining Ackermann in Coq
127. Error "Tactic failure: The relation (fun x y : BloodType => x <> y) is not a declared reflexive relation." when proving a theorem about function
128. Eval compute is incomplete when own decidability is used in Coq
129. even_Sn_not_even_n - apply 1 hypothesis in another
130. Existential goals are filled in too soon
131. Existential instantiation and generalization in coq
132. Existential quantifier in Coq impredicative logic (System F)
133. Expanding Recursive Functions In Coq
134. Explain a simple operation in Coq
135. Explanation transitivity of equal Coq
136. Extensible tactic in Coq
137. Fail to use let-destruct for tuple in Coq
138. Finding a well founded relation to prove termination of a function that stops decreasing at some point
139. Fixpoint with Prop inhabitant as argument
140. Form of intros in Coq specifically for forall and explicitly for ->
141. Function- and Type substitutions or Views in Coq
142. General advice about when to use Prop and when to use bool
143. Generalising a set of proofs in Coq
144. Generalizing existential variables in Coq
145. Generalizing expressions under binders
146. Generic equality lifting in Coq
147. Heterogeneous list in Coq
148. Hint Rewrite cannot infer parameter
149. How can I automate counting within proofs in Coq?
150. How can I avoid stack overflow or segmentation fault in Coq nats?
151. How can I construct terms in first-order logic using Coq?
152. How can I generalise Coq proofs of an iff?
153. How can I implement a Coq tactic that iterates over the hypotheses?
154. How can I prove that she cannot prove Or_commutative with only intro and apply?
155. How can I read Coq's definition of proj1_sig?
156. How can I rewrite selectively in Coq?
157. How can I use type arguments in an ltac?
158. How can I write a function of the following form in Coq?
159. How could I make example for sigma type in Coq?
160. How do I change a concrete variable to an existentially quantified var in a hypothesis?
161. How do I provide implicit arguments explicitly in Coq?
162. How do we know all Coq constructors are injective and disjoint?
163. How do you lookup the definition or implementation of Coq proof tactics?
164. How do you make notations visible outside of a module signature in Coq?
165. How do you prove in Coq that (e: p = p) = eq_refl?
166. How do you selectively simplify arguments to each time a function is called, without evaluating the function itself?
167. How does auto interract with biconditional (iff)
168. How does decidable equality works with List.remove?
169. How does one build the list of only true elements in Coq using dependent types?
170. How does one define dependent type with named arguments in Coq without issues in unification in the constructors?
171. How does one inspect what more complicated tactics do in Coq step-by-step?
172. How proof assistants are implemented?
173. How proof functions prove?
174. How to add "assumed true" statements in Coq
175. How to add to both sides of an equality in Coq
176. How to add variables introduced by set tactic to a Hint DB?
177. How to apply a function once during simplification in Coq?
178. How to convert propositional formula to DNF in Coq
179. How to deal with really large terms generated by Program Fixpoint in Coq?
180. How to debug tactic failure in a match goal branch?
181. How to define an automatically unfoldable definition
182. How to define an inductive type and a definition at the same time?
183. How to define axiom of a line as two points in Coq
184. How to define set in Coq without defining set as a list of elements
185. How to dependent match on a list with two elements?
186. How to destruct pair equivalence in Coq?
187. How to disable my custom notation in Coq?
188. How to do cases with an inductive type in Coq
189. How to do induction differently?
190. How to do induction on the length of a list in Coq?
191. How to do "negative" match in Ltac?
192. How to enumerate set in Coq Ensemble
193. How to extract the witness from exists in Coq in function notation/without destructing?
194. How to "extract" Z from subset type {z : Z | z > 0}
195. How to forbid simpl tactic to unfold arithmetic expressions?
196. How to get an induction principle for nested fix
197. How to give a counterxample in Coq?
198. How to implement a union-find (disjoint set) data structure in Coq?
199. How to import libraries in Coq?
200. How to import the library Coq.Arith.PeanoNat in Coq?
201. How to improve this proof?
202. How to introduce a new existential condition from a witness in Coq?
203. How to introduce a new variable in Coq?
204. How to leave a goal unfinished in Coq
205. How to leverage auto's searching and hint databases in custom tactics?
206. How to make algebraic manipulations in Coq easier?
207. How to make sublists in Coq?
208. How to make use of information known about this function type in Coq
209. How to match a match expression?
210. How to name the assumption when remembering an expression?
211. How to optimize a search in Coq
212. How to prove decidability of a partial order inductive predicate?
213. How to prove equality from equality of Some
214. How to prove False from obviously contradictory assumptions
215. How to prove non-equality of terms produced by two different constructors of the same inductive in Coq?
216. How to prove that a number is prime using Znumtheory in Coq
217. How to prove that another definition of permutation is the same as the Default Permutation Library for Coq
218. How to prove that terms of a first-order language are well-founded?
219. How to provide proof that two values are different?
220. How to repeat proof tactics in case in Coq?
221. How to replace a term with some property of the term?
222. How to return a (intro'd) hypothesis back to the goal formula?
223. How to save the current goal/subgoal as an assert lemma
224. How to set defaults for implicit arguments when they can't be inferred?
225. How to solve contradiction in Coq
226. How to solve goals with invalid type equalities in Coq?
227. How to specialize nested hypotheses in Coq?
228. How to specify explicit equality in Coq search patterns?
229. How to step through semicolons separated tactics sequence in coqide?
230. How to systematically normalize inequalities to < (lt) and <= (le) in Coq?
231. How to turn an single unification variable into a goal, during proof
232. How to unfold a recursive function just once in Coq
233. How to use a custom induction principle in Coq?
234. How to use an unequality to simplify a if-then-else in Coq?
235. How to use auto with repeat in custom tactics?
236. How to use modules to hide lemmas in Coq?
237. How to use rewrite on a subexpression of the current goal
238. How to use the Lemma inside a module in Coq?
239. How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 by auto but in Coq?
240. How to write to a file, from Coq
241. I need help defining a concatenation in Coq
242. Idiomatic ways of selecting subterm to rewrite
243. Implementing vector addition in Coq
244. Import vs. Include in Coq Module system
245. Improving dependently typed reverse function
246. In Coq, How to construct an element of 'sig' type
247. In Coq, how to remove a defined variable from the namespace?
248. In Coq, "if then else" allows non-boolean first argument?
249. In Coq: inversion of existential quantifier with multiple variables, with one command?
250. In Coq, is there a way to see the tactics applied by tauto?
251. In Coq, which tactic to change the goal from S x = S y to x = y
252. In-place simplification for Coq
253. In the Coq tactics language, what is the difference between intro and intros
254. Incorrect elimination of X in the inductive type or
255. Induction on predicates with product type arguments
256. Induction on record member in Coq?
257. Induction over relations
258. Induction principle for le
259. Induction proofs on MSets
260. Inductive definition for family of types
261. Inductive definition of boolean
262. Inductively defined dense vector lemmas
263. Injectivity of inl and inr in standard library
264. Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
265. Instantiating an existential with a specific proof
266. Interaction between type classes and auto tactic
267. Interactive theorem proving with no specified goal
268. Inversion produces unexpected existT in Coq
269. Inverting an obviously untrue hypothesis does not prove falsehood
270. Is it possible to declare type-dependent Notation in Coq?
271. Is it possible to force induction tactic to produce more equations?
272. Is there a eapply-like tactic that works on exists goals in Coq?
273. Just a universally quantified hypotesis in Coq proof
274. Lemma about list and rev list
275. Lemma as a type in a record
276. Less or equal relation with largest element of natural number list
277. Lift existentials in Coq
278. Local Inductive definitions and Theorems
279. Locating definition of a tactic in Coq proofs
280. Logic: auxilliry lemma for tr_rev_correct
281. Ltac: optional arguments tactic
282. Ltac pattern matching: why does forall x, ?P x not match forall x, x?
283. make subset types compatible for function application
284. Matching expression context under forall with Ltac
285. Matching with Ltac on a call containing local variable
286. Merge duplicate cases in match Coq
287. Multiple successes in Coq branching and backtracking?
288. Multiple where-clauses for Reserved Notation in Coq?
289. mutual recursion on an inductive type and nat
290. Nested recursion and Program Fixpoint or Function
291. Non-positive occurrence due to polymorphic function
292. Pattern-match on type in order to implement equality for existentially typed constructor in Coq
293. Pattern matching using information from theorems
294. Pattern Matching with Even and Odd Cases
295. Pigeonhole proof without decidable equality or excluded middle
296. Port a Coq lemma over Z to a similar lemma over nat
297. Pose proof in Coq
298. Problems with dependent types in Coq proof assistant
299. Problems with missing information in Obligations when defining using Program in Coq
300. Program Fixpoint: recursive call in let and hypothesis of the obligation
301. Proof automation in Coq how to factorize a proof
302. Proof automation
303. Proof by case analysis in Coq
304. Proof by contradiction in Coq
305. Proof leaking in Coq extraction?
306. Proof of the application of a substitution on a term
307. Proofs about constructors matched with _
308. Proofs of structural properties of arguments in match in coq
309. Prove a constant is even
310. Prove equality on Sigma-types
311. Prove properties of lists
312. Prove that the only zero-length vector is nil
313. Proving a property on sets
314. Proving decidability for a datatype that includes a vector
315. Proving equivalence of two programs expressed as different types
316. Proving even + even = even with mutual induction using tactics
317. Proving False with negative inductive types in Coq
318. Proving forall x xs ys, subseq (x :: xs) ys -> subseq xs ys in Coq
319. Proving increasing iota in Coq
320. Proving termination in Coq
321. Proving Termination of Function in Coq
322. Proving that s-expressions printing is injective
323. Proving uniqueness of an instance of an indexed inductive type
324. Question about intros [=] and intros [= <- H]
325. Reasoning about lists in Coq
326. Reasoning about typeclass instance that has been picked up in a theorem?
327. Record and Definition
328. Record equality in Coq
329. Recursion for Church encoding of equality
330. Recursive partial functions in Coq
331. Recursive use of typeclass methods in Coq
332. Redundant clause in match
333. Relation between types prod and sig in Coq
334. Removing the last element of a sized list in Coq
335. Removing trivial match clause in Coq
336. Renaming part of hypothesis in Coq
337. Representing Higher-Order Functors as Containers in Coq
338. Require, Import, Require Import
339. Retrieving constraints from GADT to ensure exhaustion of pattern matching in Coq
340. Returning a record from a definition in Coq
341. Rewrite single occurence in Ltac
342. Rewrite under exists
343. rewrite works for = but not for <-> (iff) in Coq
344. Rewriting hypothesis to false with a contradictory theorem
345. Section mechanism in Coq. Forbid omitting of hypotheses from context
346. SF Volume 1: Logic: How to prove tr_rev <-> rev?
347. Shorter notation for matching hypotheses in Coq?
348. Show all axioms Coq
349. Show theorem definition in Coq
350. Some help dealing with inject/unject and vector types
351. Specialization of module argument in Coq
352. Split conjunction goal into subgoals
353. Step by step simplification in Coq?
354. Stronger completeness axiom for real numbers in Coq
355. Structural recursion on two arguments
356. Stuck on a simple proof about regular expressions
357. Stuck on the proof of a simple Lemma: which induction should I use?
358. Subset parameter
359. Subtyping in Coq
360. Syntax error with < in Coq notations
361. Tactic automation: simple decision procedure
362. Teach Coq to check termination
363. Transferring proof from Z to N in Coq
364. Transform casual list into dependently typed list in Coq
365. Transitivity of -> in Coq
366. Transitivity of subsequence in Coq
367. Trouble writing my notation for natural numbers in Coq
368. Turn off automatic induction principle in Coq
369. Type encapsulation in Coq
370. Typeclass resolution and autorewrite
371. Typeclasses with multiple fields vs. single field in Coq / Unexpected behaviour of Compute command
372. Unable to find an instance for the variable
373. Under what conditions does Eval cbv delta in expand a definition in Coq?
374. Understanding how pattern matching works in Coq
375. Understanding specialize tactic
376. Understanding the intros keyword work in Coq
377. Understanding "well founded" proofs in Coq
378. Unfold a notation within a scope
379. Unfold notation in ltac
380. Use module signature definition in module implementation
381. Using an existential theorem in Coq
382. Using dependent induction tactic to keep information while doing induction
383. Using dependent types in Coq (safe nth function)
384. Using Implicit Type Class Parameters in Coq Notation
385. Using induction starting from 1 in Coq
386. Using length of list X as an argument for a constructor of X in Coq
387. Using local notation inside a Coq theorem
388. Using Omega to prove a lemma in Coq
389. Using typeclass instances within typeclasses
390. Vector error: The type of this term is a product
391. Vector : t A n = t A (n+0)?
392. "Verbose" auto in Coq
393. Wellfounded induction in Coq
394. What does it mean when Coq expands a function as part of the goal?
395. What does Proof. simpl. reflexivity. Qed. mean in Coq?
396. What does the tactic destruct do in the proof below?
397. What does the tactic induction followed by a number do?
398. What is a concrete example of the type Set and what is the meaning of Set?
399. What is Coq's type system doing in this example?
400. What is difference between destruct and case_eq tactics in Coq?
401. What is eq_rect and where is it defined in Coq?
402. What <> is in Coq
403. What is the difference between Axiom and Variable in Coq
404. What is the difference between Lemma and Theorem in Coq
405. What is the tactic that does nothing?
406. What should be done when simpl does not reduce all the necessary steps?
407. What's the difference between Program Fixpoint and Function in Coq?
408. What's the difference between revert and generalize tactics in Coq?
409. When are the constructors of an inductive type exhaustive?
410. Where did lt_index go?
411. Which vector library to use in Coq?
412. Why are logical connectives and booleans separate in Coq?
413. Why can I not apply f_equal to a hypothesis?
414. Why can I use the constructor tactic to prove reflexivity?
415. Why can't Coq infer the that 0 + n = n in this dependently typed program?
416. Why can't I define the following CoFixpoint?
417. Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
418. Why do Calculus of Construction based languages use Setoids so much?
419. Why does Coq.Init.Logic define the notation A -> B?
420. Why does Coq's typechecker reject my map definition?
421. Why does nesting the induction tactic also nest the inductive hypotheses under a lambda?
422. Why does this Coq Definition fail? Coq Namespace error for Inductive Type
423. Why does use of Coq's setoid_replace ... by clause need an extra idtac?
424. Why haven't newer dependently typed languages adopted SSReflect's approach?
425. Why is following Coq rewrite not applying on right hand side of assumption?
426. Why is my recursive definition of list_min ill-formed?
427. Why not have Prop : Set in Coq?
428. Why S n' =? S n' simplifies to n' =? n' in Coq?
429. Why would the tactic exact be complete for Coq proofs?