Skip to main content
Proof Assistants Beta
Pierre Jouvelot's user avatar
Pierre Jouvelot's user avatar
Pierre Jouvelot's user avatar
Pierre Jouvelot
  • Member for 2 years, 5 months
  • Last seen more than a week ago
  • Paris, France
Profile Activity
Stats
271
reputation
2k
reached
8
answers
0
questions
Communities
About

My homepage

Badges
This user doesn’t have any gold badges yet.
1
silver badge
3
bronze badges
Top tags
17
Score
8
Posts
100
Posts %
5
Score
2
Posts
25
Posts %
5
Score
2
Posts
25
Posts %
4
Score
1
Posts
12
Posts %
1
Score
1
Posts
12
Posts %
1
Score
1
Posts
12
Posts %
Top posts
6
Are there any ergonomic ways to deal with finite types in Coq?
Jan 15, 2023
4
How to prove `forall m n : nat, m == n -> m = n`?
Feb 17, 2022
2
How to to use the fact that combining these hypothesis is false in Coq
Dec 10, 2023
1
In Coq, what tactic can I use to remove a True precondition from a hypothesis
Mar 18
1
In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?
Jan 25, 2023
1
How to provide a countType when using mathcomp?
Apr 13, 2022
1
Why use records for non-empty lists rather than inductively defined non-empty lists?
Jul 3, 2022
1
How do I approach the final inductive step in `plus_leb_compat_l` from Software Foundations?
Dec 25, 2022
Top network posts
View all network posts
6
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?