coq

coq copied to clipboard

Extend "discriminate" so it can handle impossible equations such as n = S n

7

As @herbelin said [here](https://github.com/coq/coq/pull/19475#pullrequestreview-2278374479): > On the other side, I'm unsure we have to be proud that cyclic equalities are not automatically found contradictory. If not by `discriminate`, there should...

jfehrle

### Description of the problem I write a Coq project managing a lot of list equalities containing `++`. To simplify rewriting hypothesis into such list equalities, I use a package...

JulesViennotFranca

Variant of discriminate that refutes statements such as "S n <= 0"

3

### Is your feature request related to a problem? Tactic `discriminate` is able to refutes `S n = 0` and it does it by mapping `S n` to `True` and...

herbelin

discriminate and injection do not work with sort polymorphic inductive types

1

### Description of the problem the `discriminate` and `injection` tactics are not compatible with sort polymorphic inductive types instantiated at `Type` ### Small Coq file to reproduce the bug ```coq...

tabareau

[config] Re-enable use of configure option -bytecode-compiler

3

Since #16931 , `./configure -bytecode-compiler no` had no effect, as we stopped checking the flag. We do instead like native and set default options flag. I wonder if these options...

ejgallego

Fixpoint inside a lemma produces anomaly universe undefined

3

### Description of the problem Consider this little example: ~~~coq From Coq Require Import FinFun. From Coq Require Import Classes.Equivalence. Definition f_id {X: Type} (x0: X) := x0. Lemma simpl_prop:...

svyatlovskiy

discriminate is weaker than injection;discriminate with impredicative set

3

~~~coq (* -*- coq-prog-args: ("-impredicative-set"); -*- *) Inductive X : Set := x : Type -> bool -> X. Goal x bool true x bool false. red. Fail discriminate. injection....

SkySkimmer

"induction" may drop hypothesis if it's a Prop

1

### Description of the problem `induction IHm` drops `IHm` from the context. It should give a error and make no change if that's not too hard.  ### Small Coq...

jfehrle

Universe inconsistency involving template poly and canonical structure since 8.21

15

### Description of the problem Between `8.20.0` and current `8.21+alpha` for (to me) unclear reasons there are universe inconsistencies in [coq-library-undecidability](https://github.com/uds-psl/coq-library-undecidability/tree/master). ### Small Coq file to reproduce the bug ```coq...

mrhaandi

8.18 and 8.19 docs use the branch version instead of the tag

2

So the URL is https://coq.inria.fr/doc/v8.19/refman/ instead of https://coq.inria.fr/doc/V8.19.2/refman/ also https://coq.inria.fr/doc/v8.19/refman/changes.html has an "unreleased changes" section at the beginning Is using the branch deliberate?

SkySkimmer