Skip to main content
Proof Assistants Beta
Lolo's user avatar
Lolo's user avatar
Lolo's user avatar
Lolo
  • Member for 2 years, 5 months
  • Last seen more than a month ago
Profile Activity

18 Answers

Score Activity Newest
7 votes

How does the formal proof of the four color theorem work?

5 votes
Accepted

Why can't I use let bindings to pattern match a 3-tuple in Coq?

3 votes
Accepted

Destruction of bound dependent types

3 votes
Accepted

How to prove this correctness principle of transposition of lists of lists in Coq?

2 votes

How to correctly feed type argument in this toy theorem?

2 votes

How do I prove this theorem with induction in COQ

1 vote

How do I prove an expression in Coq that involves pattern matching?

1 vote
Accepted

How to convert hypothesis with "if then else" equality into its consequent using coq?

1 vote

In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?

1 vote
Accepted

What is the idiomatic way in Coq to write recursive functions over product types?

1 vote
Accepted

How to apply constructor injectivity in the goal

0 votes

How to prove basic lemmas about divisibility in Coq?

0 votes
Accepted

Coq: Proving snd divmod doesn't depend on parameter q?

0 votes

Induction COQ Question

0 votes

Help with strong induction

0 votes

How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

0 votes

How to get rid of opaque proof-terms in computation

0 votes

Destructing transitivity hypothesis on simple predicate logic