Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

discriminate and congruence cannot distinguish primitive values #20011

Open
Janno opened this issue Jan 10, 2025 · 0 comments
Open

discriminate and congruence cannot distinguish primitive values #20011

Janno opened this issue Jan 10, 2025 · 0 comments
Labels
kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: congruence The congruence tactic. part: tactics

Comments

@Janno
Copy link
Contributor

Janno commented Jan 10, 2025

Description of the problem

No response

Small Rocq / Coq file to reproduce the bug

Require Import Stdlib.Numbers.Cyclic.Int63.PrimInt63.
Require Import Stdlib.Floats.PrimFloat.
Require Import Stdlib.Array.PArray.
Require Import Stdlib.Strings.PrimString.

Goal
  (1 = 1)%uint63 ->
  (1.0 = 1.0)%float ->
  [|tt | tt |] = [| | tt|] ->
  ("true" = "false")%pstring ->
  False
.
Proof.
  Fail congruence.
  Fail discriminate.
Abort.

Version of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response
@Janno Janno added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: tactics part: congruence The congruence tactic. labels Jan 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: congruence The congruence tactic. part: tactics
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Janno