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.

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

Printing part of numeral notation does not work in all cases. #9840

Closed
Zimmi48 opened this issue Mar 27, 2019 · 35 comments · Fixed by #9874

Comments

@Zimmi48
Copy link
Member

commented Mar 27, 2019

Description of the problem

While in the following case, the printing part of numeral notations works fine:

Record a := { n : nat ; p : True }.

Definition to_a i := Build_a (Nat.of_uint i) I.
Definition of_a '(Build_a n _) := Nat.to_uint n.

Numeral Notation a to_a of_a : foo_scope.

Open Scope foo_scope.

Check 1.

(* 1
     : a
*)

in these variations, it does not:

Axiom h : False.

Record a := { n : nat ; p : False }.

Definition to_a i := Build_a (Nat.of_uint i) h.
Definition of_a '(Build_a n _) := Nat.to_uint n.

Numeral Notation a to_a of_a : foo_scope.

Open Scope foo_scope.

Check 1.

(* {| n := 1; p := h |}
     : a
*)
Record a := { n : nat ; p : or True False }.

Definition to_a i := Build_a (Nat.of_uint i) (or_introl I).
Definition of_a '(Build_a n _) := Nat.to_uint n.

Numeral Notation a to_a of_a : foo_scope.

Open Scope foo_scope.

Check 1.

(* {| n := 1; p := or_introl I |}
     : a
*)
Parameter A : Prop.
Axiom h : A.

Record a := { n : nat ; p : A }.

Definition to_a i := Build_a (Nat.of_uint i) h.
Definition of_a '(Build_a n _) := Nat.to_uint n.

Numeral Notation a to_a of_a : foo_scope.

Open Scope foo_scope.

Check 1.

(* {| n := 1; p := h |}
     : a
*)
Record a := { n : nat ; p : 0 = 0 }.

Definition to_a i := Build_a (Nat.of_uint i) eq_refl.
Definition of_a '(Build_a n _) := Nat.to_uint n.

Numeral Notation a to_a of_a : foo_scope.

Open Scope foo_scope.

Check 1.

(* {| n := 1; p := eq_refl |}
     : a
*)

Found by @roglo while trying to use numeral notations for his rational numbers.

cc @JasonGross

Coq Version

8.9.0

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Numeral Notations only print ground terms; this is in some sense a feature, because we don't want to spend a lot of time fully normalizing fixpoints when reduction is blocked.

The failure with eq_refl is probably a missing case in the conversion to/from glob_constr. I'm guessing it's a missing case for inductive type families, and it's probably safe to add such a case.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

The case eq_refl is indeed the one I need. My rationals contain a proof that num and den are coprimes, that is a proof of equality between two nats (gcd n d = 1).

@JasonGross

This comment was marked as outdated.

Copy link
Contributor

commented Mar 27, 2019

I don't know the relevant bits of the API (and don't have time to dig into it right now), but I believe if you add a case for inductive type families to

coq/interp/notation.ml

Lines 645 to 655 in 738521c

let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
| App (c, ca) ->
let c = glob_of_constr token_kind ?loc env sigma c in
let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in
DAst.make ?loc (Glob_term.GApp (c, cel))
| Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
| Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
| Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
| Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
| Int i -> DAst.make ?loc (Glob_term.GInt i)
| _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))

then the printing should work.

Edit: oh, it has a case for Ind. You may need to add a case for Sorts, but this might not actually be the issue. Let me look at the code a bit more.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Okay, I think I actually found the issue this time. I think a case for Ind should be added to

coq/interp/notation.ml

Lines 633 to 643 in 738521c

let rec constr_of_glob env sigma g = match DAst.get g with
| Glob_term.GRef (ConstructRef c, _) ->
let sigma,c = Evd.fresh_constructor_instance env sigma c in
sigma,mkConstructU c
| Glob_term.GApp (gc, gcl) ->
let sigma,c = constr_of_glob env sigma gc in
let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
sigma,mkApp (c, Array.of_list cl)
| Glob_term.GInt i -> sigma, mkInt i
| _ ->
raise NotAValidPrimToken

I don't have time right now you figure out what the right line to add is, but I imagine anyone familiar with constr and glob_constr should not have much trouble adding the correct line.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Seems to resolve the case when the type is 0=0 as for Theo's example, but not mine: my type is, roughly (n, d, Nat.gcd n d = 1).

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

I think this is part of the feature: we don't try to print things that are not ground. Try either using 1 = Nat.gcd n d or else explicitly fill the term with eq_refl nat 1.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Note: we should also document this in the section on numeral notations, because it is at least a little subtle.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Changing my (Nat.gcd x y = 1) into (1 = Nat.gcd x y) in my definition, I get now,, when I try to print 5%Q

Error: Unexpected term
match
  PQ.PQred_gcd {| PQ.PQnum1 := 4; PQ.PQden1 := 0 |} in (_ = H) return (H = 1)
with
| eq_refl => eq_refl
end while parsing a numeral notation.
@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Yeah, you need to make sure your parsing function is fully transparent. There's a trick for making proofs of equalities that are decidable transparent: write a transparent decider (I think decide equality and Scheme Equality give you something that is fully transparent in most cases), and then use the given proof of equality (which can be opaque) to do False-elimination only when the equality decider says "not equal".

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

Too complicated for me. Trying to change "Qed" into "Defined" in PQred_gcd, I now get a lot of insults starting with "Error: Unexpected term...". And, I am sorry, your explanations are just Coq jargon for me. Theo and Hugo try to explain me too, it is exactly if they spoke greek to me.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

What does "False-elimination" mean? I have been coding in Coq since eight years, I never eliminated False. Anyway it is defined in the standard library. How can I eliminate it?

@SkySkimmer

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

The idea is to only block on potentially opaque values when you're in some absurd branch (in which case a standard way to fill the branch is to prove False and eliminate the proof).
ie consider this example

Lemma beq_sym : forall {b1 b2 : bool}, b1 = b2 -> b2 = b1.
Proof.
  intros b1 b2 H;destruct b1,b2;try reflexivity;discriminate. (* only eliminate the equality in true = false / false = true cases *)
Defined.

(* some arbitrary blocking value, in your case from PQred_gcd I guess *)
Lemma opaque_eq : true = true.
Proof.
  reflexivity.
Qed.

Eval compute in eq_sym opaque_eq. (* eq_sym is https://github.com/coq/coq/blob/738521ca3acb0f5b87cb1d23360350ed69f18cd1/theories/Init/Logic.v#L372-L375 *)
(*     = match opaque_eq in (_ = y) return (y = true) with
       | eq_refl => eq_refl
       end
     : true = true
 *)

Eval compute in  beq_sym opaque_eq.
(* = eq_refl
     : true = true
*)

(* we get the opposite blocking when the boolean is abstract but the proof is eq_refl: *)
Section Foo.
  Variable b : bool.
  Eval compute in eq_sym (@eq_refl _ b). (* = eq_refl *)
  Eval compute in beq_sym (@eq_refl _ b). (* = some horrible term *)
@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

@roglo Here is the definition I was suggesting:

Definition transparent_nat_eq_dec (n m : nat) : {n = m} + {n <> m}.
Proof. decide equality. Defined.

Definition transparentify_nat_eq {n m : nat} (H : n = m) : n = m
  := match transparent_nat_eq_dec n m with
     | left pf => pf
     | right npf => match npf H with end (* False-elimination *)
     end.

Axiom H : 1 = 1.
Compute transparentify_nat_eq H. (* eq_refl *)
@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

If you make sure to apply transparentify_nat_eq to the equality proof of 1 = Nat.gcd x y before inserting it into your record when canonicalizing your rationals, then they should parse (and print) fine.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 27, 2019

And, I am sorry, your explanations are just Coq jargon for me.

And sorry about this. I have learned to think in Coq, so I sometimes struggle a bit when trying to translate my thoughts into comprehensible speech.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

OK, your trick works. Thank you!

Nevertheless, I am not sure I keep it because it supposes to change the definition of my rationals, making it less clear and simple: I don't like the 1=gcd instead of gcd=1 nor the transparency stuff.

I must think of it.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

I don't like the 1=gcd instead of gcd=1

You can instead of this explicitly write eq_refl 1 rather than just eq_refl.

There is no similar simple trick I'm aware of for the transparency stuff

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

You can instead of this explicitly write eq_refl 1 rather than just eq_refl.

Where? I see that the proof value of my rationals magically became "eq_refl" indeed, but I did not put this "eq_refl" myself in my code. There is no such explicit "eq_refl" in yours.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

This is very mysterious for me. How can "eq_refl" can be a proof of gcd x y = 1? The two terms are not identical! However, I see it in my code, when using the trick.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

With a little help from my friend Hugo, to make it work, we added two cases (and not only one) in constr_of_glob, Ind and Const, and it works even for gcd a b = 1.

But he claims that the problem is because of this silly conversion between constr and glob_contr which should not be required in an ideal world.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

I am quite reluctant to allow Const; I fear this may print S (1 + 2) as 4 (does it?), and also may cause arbitrary slow-downs as Coq tries to normalize in the vm terms that are not ground and have enormous normal forms.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

If you point me at your code, I may be able to explain more about where eq_refl comes from.

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

Record GQ :=
  GQmake0
    { PQ_of_GQ : PQ;
      GQprop : Nat.gcd (PQnum1 PQ_of_GQ + 1) (PQden1 PQ_of_GQ + 1) = 1 }.
Arguments GQmake0 PQ_of_GQ%PQ.
Arguments PQ_of_GQ x%GQ : rename.

Definition transparentify {A} (D : {A} + {¬A}) (H : A) : A :=
  match D with
  | left pf => pf
  | right npf => match npf H with end
  end.

Definition GQmake x p := GQmake0 x (transparentify (Nat.eq_dec _ _) p).
Arguments GQmake x%PQ.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

And this does not work without Const... Hm... Does it work without the Const case if you change the call to the vm to a call to cbv by swapping which definition is commented out in

coq/interp/notation.ml

Lines 611 to 622 in 738521c

let eval_constr env sigma (c : Constr.t) =
let c = EConstr.of_constr c in
let sigma,t = Typing.type_of env sigma c in
let c' = Vnorm.cbv_vm env sigma c t in
EConstr.Unsafe.to_constr c'
(* For testing with "compute" instead of "vm_compute" :
let eval_constr env sigma (c : Constr.t) =
let c = EConstr.of_constr c in
let c' = Tacred.compute env sigma c in
EConstr.Unsafe.to_constr c'
*)

? (Hypothesis: the vm does not normalize parameters of inductives when they show up in constructors, IIRC)

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

It works indeed by swapping the comments in your code above.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

Okay, I think you (or someone) should propose the PR that adds an Ind case and uses cbv rather than the vm (and adds a comment linking to this issue / explaining the context about why we should confine to use cbv and not the vm). IIRC, @ejgallego may already have proposed a PR switching from vm to cbv?

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

Mmmm... eventually... that does not work so well. It works at the beginning, just with testing simple cases like 1%Q or 5%Q, but later, I have problems in the proofs, the values are not recognized and theorems refuse to be applicated.

It is not due to your change, it does not work with my changes either. I remove (comment) my Numeral Notation for the moment, I see that later.

Perhaps, @herbelin 's idea would work better (removing glob_of_constr & constr_of_glob and rather keep the Constr.t in DAst, something like that).

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

@roglo What makes you think that @herbelin 's idea would work better? I think the terms end up being the same either way...

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

Ah ok.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

@roglo Do you have [a pointer to] the code for the Ind case? I'd like to submit it as a PR

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

It is useless, since the whole thing does not work.

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

I think it is still potentially useful for other applications, e.g., a numeral notation for a list of nat digits.

I may also be able to help with getting more it two work in your case, if you supply more details (either here or on gitter or elsewhere).

@roglo

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

let rec constr_of_glob env sigma g = match DAst.get g with
   | Glob_term.GRef (ConstructRef c, _) ->
       let sigma,c = Evd.fresh_constructor_instance env sigma c in
       sigma,mkConstructU c
+  | Glob_term.GRef (IndRef c, _) ->
+      let sigma,c = Evd.fresh_inductive_instance env sigma c in
+      sigma,mkIndU c
   | Glob_term.GApp (gc, gcl) ->
       let sigma,c = constr_of_glob env sigma gc in
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Mar 31, 2019

Thanks!

JasonGross added a commit to JasonGross/coq that referenced this issue Mar 31, 2019
[interp] [numeral] Use cbv rather than vm
It is important to fully normalize the term, *including inductive
parameters of constructors*; see coq#9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.

Supersedes / closes coq#9655
JasonGross added a commit to JasonGross/coq that referenced this issue Mar 31, 2019
JasonGross added a commit to JasonGross/coq that referenced this issue Mar 31, 2019
JasonGross added a commit to JasonGross/coq that referenced this issue Mar 31, 2019
JasonGross added a commit to JasonGross/coq that referenced this issue Apr 1, 2019
[interp] [numeral] Use cbv rather than vm
It is important to fully normalize the term, *including inductive
parameters of constructors*; see coq#9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.

Supersedes / closes coq#9655
JasonGross added a commit to JasonGross/coq that referenced this issue Apr 1, 2019
JasonGross added a commit to JasonGross/coq that referenced this issue Apr 1, 2019
@roglo

This comment has been minimized.

Copy link
Contributor

commented Apr 1, 2019

I managed to make the thing work, with the two changes. But there is a problem of unification while applying theorems. I have a theorem saying, e.g. that forall n, (n / 1 = this or that)%Q. But when I try to apply it on (1 = this or that)%Q, it says it cannot. I am just allowed to apply with (1 / 1 = this or that)%Q. Because in 1%Q, the proof part is eq_refl (thanks to your advices), but in (1/1)%Q, it is not. The unification fails. I found two possible solutions : first writing replace 1%Q with (1/1)%Q by easy (which works) before the call, or second, calling the theorem by giving explicitely the value of n (e.g. with (n := 1)).

@Zimmi48 Zimmi48 added this to the 8.9.1 milestone Apr 26, 2019

@Zimmi48 Zimmi48 modified the milestones: 8.9.1, 8.10+beta1 May 17, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.