Program tactic and equations

[spitters]

It would be nice to have Program for HoTT, e.g. for use in HoTT-Classes. I keep on forgetting what we have done already.

There was a discussion here: https://github.com/HoTT/HoTT/commit/6a99db1c31fe267fdef7be755fa169fb6a87e3cf

However, it would be really nice to combine this with the Equations plugin by @mattam82 and @cmangin.

[spitters]

https://mattam82.github.io/Coq-Equations/

[mattam82]

Note that Equations currently cannot be used directly with the HoTT library as it compiles against the standard library but can surely be made independent.

[spitters]

Do you or @cmangin (or @SkySkimmer for that matter) have any plans of doing that in the future. HoTT seems to be an ideal application for Equations.

[mattam82]

I’ve tried a little bit and it’s mostly an engineering issue, so any help would be appreciated! Le jeu. 16 nov. 2017 à 08:20, Bas Spitters notifications@github.com a écrit :

Do you or @cmangin https://github.com/cmangin (or @SkySkimmer https://github.com/skyskimmer for that matter) have any plans of doing that in the future. HoTT seems to be an ideal application for Equations.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/895#issuecomment-344837090, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARbnTvbegcwEYpHRfnvH8fHc-tQHHks5s2-ImgaJpZM4PUtGC .

[spitters]

Recording an email discussion with @mattam82

the main issue is binding of the constants used by Equations, and probably a bit of fidling with the current Coq proofs the theories/ library which might use tactics that are broken with an equality in Type (though unlikely now). The binding is mostly straightforward, for general constants everything is done in src/equations_common.ml

let coq_unit = lazy (init_reference ["Coq";"Init";"Datatypes"] "unit") let coq_tt = lazy (init_reference ["Coq";"Init";"Datatypes"] "tt") let coq_Empty = lazy (init_reference ["Coq";"Init";"Datatypes"] "Empty_set") ... https://github.com/mattam82/Coq-Equations/blob/master/src/equations_common.ml

However, this are currently unavailable in: https://github.com/HoTT/HoTT/blob/master/coq/theories/Init/Datatypes.v They are here: https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v

An issue is maintainability. Should we have a binding in a .v file like Agda's PRAGMA BUILTIN or Equations Logic command?

I wonder how this is treated by @SkySkimmer in his sProp work.

[SkySkimmer]

What does this have to do with SProp?

[spitters]

I meant: you are also introducing a new class of propositions. Do the stdlib and all the tactics continue to work out of the box? If not, how do you plan to maintain your patched version of Coq?

[andreaslyn]

Hi @spitters. I have looked a bit into porting Equations to HoTT, https://github.com/mattam82/Coq-Equations/compare/8.8+alpha...andreaslyn:hott-port?expand=1. I am currently working on building Equations with HoTT, which is challenging. Equations depends on tactics from Program, they probably need to be ported as well. I think the first task is to make Equations build with HoTT. Afterwards I can find the lemmas in HoTT corresponding to the constants which are dynamically referenced by Equations, then I will be able to test it. I would like to get some feedback to make sure I am doing in the right direction.

[spitters]

I think it's a good start. Not sure what to do about congruence. @mattam82 ?

[andreaslyn]

Fixing congruence seems to be the next step in porting Equations to HoTT. I can take a look at it, but I am not sure how tricky it is, and I do not have much time I can put into this.

[mattam82]

Hmm that would be harder, as congruence is quite complicated code relying crucially on the structure of equality. However, I think congruence is only used in the old compilation path that is still present, and maybe in some proofs that can be done without it. So you should be able to simply remove it. Le mer. 7 mars 2018 à 12:01, Andreas Lynge notifications@github.com a écrit :

Fixing congruence seems to be the next step in porting Equations to HoTT. I can take a look at it, but I am not sure how tricky it is, and I do not have much time I can put into this.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/895#issuecomment-371164200, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARQ7hZqVV8K4Gs8vQYEobbL1xh4bLks5tb_TpgaJpZM4PUtGC .

[mattam82]

About the tactics from Program, I think it can be made independent as well. Le mer. 7 mars 2018 à 17:49, Matthieu Sozeau mattam@mattam.org a écrit :

Hmm that would be harder, as congruence is quite complicated code relying crucially on the structure of equality. However, I think congruence is only used in the old compilation path that is still present, and maybe in some proofs that can be done without it. So you should be able to simply remove it. Le mer. 7 mars 2018 à 12:01, Andreas Lynge notifications@github.com a écrit :

Fixing congruence seems to be the next step in porting Equations to HoTT. I can take a look at it, but I am not sure how tricky it is, and I do not have much time I can put into this.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/895#issuecomment-371164200, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARQ7hZqVV8K4Gs8vQYEobbL1xh4bLks5tb_TpgaJpZM4PUtGC .

[andreaslyn]

Sounds good. Thank you for the input.

[andreaslyn]

Hi @mattam82. I have some problems with porting Equations to HoTT related to universes. I hope you can find some time to help with this. I have created a script which can setup everything so you can get started fast on a Unix system.

You can can fetch my branch with: git clone -b hott-port https://github.com/andreaslyn/Coq-Equations.git path/to/andreas-equations with diff https://github.com/mattam82/Coq-Equations/compare/8.8+alpha...andreaslyn:hott-port?expand=1

I have added the build.sh script which you can use to clone HoTT to path/to/andreas-equations/custom-HoTT, and afterwards it will patch this HoTT. Use: path/to/andreas-equations/build.sh HoTT to build this patched version of HoTT. Note that it uses 4 makefile threads, but it is easy to change in build.sh. Use: path/to/andreas-equations/build.sh Eq to build Equations.

For interactive mode you can use the executable path/to/andreas-equations/custom-HoTT/hoqtop.

I have commented out some places where I get Anomaly "Universe ... undefined": theories/NoConfusion.v: line 70 theories/NoConfusion.v: line 74 theories/Fin.v: line 21

I have also commented out a place where I get "Universe ... is unbound": theories/EqDecInstances.v: line 74

[mattam82]

I looked at NoConfusion.v:L70 and indeed there is an issue with how we derive NoConfusion for polymorphic inductives. I've made some progress there but it's not the end of the story: https://github.com/mattam82/Coq-Equations/tree/hott-port

[mattam82]

For fin this is a workaround (I didn't track the bug yet): Inductive fin@{} : nat -> Set := | fz : forall {n : nat}, fin (S n) | fs : forall {n : nat}, fin n -> fin (S n).

I pushed a patch doing just that. There's a weird behavior of requiring {n : nat} to be specified, looks to me like a Coq bug.

[mattam82]

There seems to be a general problem with "Derive" not being able to automatically solve the polymorphic obligations even if the tactics work. Maybe a bug in handling of obligations in Coq. E.g in EqDecInstances the proofs can be derived using "eqdec_proof".

The next one can be fixed (patch on my tree as well)

[andreaslyn]

Thanks a lot. I can make more progress now.

[andreaslyn]

Hi @mattam82. We do not need the fin@{} workaround anymore, but I have made a list of other problems which I am not sure how to deal with. When you have some time, it would be nice if you could help out with some of problems listed below. Note that we still have the build script, see https://github.com/HoTT/HoTT/issues/895#issuecomment-375335206.

1. In theories/NoConfusion.v: 72. The behavior of Derive is not the same when building with make as in interactive mode.
2. I think that Ltac funind is not working. See theories/Fin.v: 43.
3. In theories/EqDecInstances.v: 34, Ltac eqdec_proof is using inversion which is not working.
4. Derive Below for nat gives error in theories/Below.v: 74.
5. Universe error in examples/Basics.v: 55.

[spitters]

Since you are working on Equations. It may help to include @cmangin .

[andreaslyn]

@spitters @mattam82 @cmangin. There are problems with the code generated by Derive NoConfusion and Derive Below. In NoConfusion.v:106 it fails with error message "Pattern-matching expression on an object of inductive type @sig has invalid information".

It fails because is_primitive_record spec returns true at kernel/inductive.ml:395. Here is a stack trace:

Noconf.derive_no_confusion
Equations_common.make_definition
Typing.e_type_of
Typing.execute
Typing.e_judge_of_case
Inductive.check_case_info

In Below.v:74 it fails with Anomaly "Universe Var(0) undefined" at kernel/uGraph.ml:136. The stack trace is:

Subterm.derive_below (last expression)
Equations_common.declare_constant
Equations_common.make_definition
Typing.e_type_of
Typing.execute
Typing.e_judge_of_apply
Evarconv.e_cumul
Evarconv.evar_conv_x
Reductionops.infer_conv
Reductionops.infer_conv_gen
Evd.add_universe_constraints
Evd.add_universe_constraints_context
UState.add_universe_constraints
UState.process_universe_constraints
UGraph.check_leq
UGraph.real_check_leq
UGraph.exists_bigger
UGraph.check_smaller_expr
UGraph.check_smaller
UGraph.repr
CErrors.anomaly

In examples/Basics.v:55 it fails with the same Anomaly "Universe Var(0) undefined" at kernel/uGraph.ml:136. The stack trace is different though.

Maybe these errors are related?

I have created a branch hott-port-debug which demonstrates that the Derive commands work when using custom code, theories/Debug.v, rather than the code generated by the Derive commands. The files NoConfusion.v and Below.v compile in this branch.

[mattam82]

The first bug should be fixed by my latest commit on equations (8.8 or master). The second one about universes I need to look into.

[andreaslyn]

There is a problem when calling Equations_common.declare_constant with poly=true. For example, in Subterm.derive_below right after

 let below = declare_constant id bodyB None polymorphic !evd
    (Decl_kinds.IsDefinition Decl_kinds.Definition) in

I have tried to add the following debug statements:

  let () = Feedback.msg_debug (Printer.pr_econstr (Typing.e_type_of (Global.env ()) evd (bodyB))) in
  let () = Feedback.msg_debug (Printer.pr_econstr (Typing.e_type_of (Global.env ()) evd (mkConst below))) in

The first debug message was ((Bool -> Type@{Equations.Below.38}) -> Bool -> Type@{Equations.Below.38}). I would expect the second debug message to be the same, but it was ((Bool -> Type@{Var(0)}) -> Bool -> Type@{Var(0)}).

When invoking Equations_common.declare_constant with poly=false then this issue is not present.

[SkySkimmer]

That's because mkConst on a polymorphic constant is wrong. I'm actually surprised that Typing doesn't even check instance length, much less polymorphic constraints.

[andreaslyn]

Is there a bug on the following lines? https://github.com/mattam82/Coq-Equations/blob/4cbc0e8f85f50a1d56a0af289a72da0e711f34f3/src/subterm.ml#L362 https://github.com/mattam82/Coq-Equations/blob/4cbc0e8f85f50a1d56a0af289a72da0e711f34f3/src/subterm.ml#L371

[mattam82]

Indeed it is buggy, we should rather use Evarutil.fresh_global or some such function to get an instance of the polymorphic below constant and register it’s universes in the evd variable.

[andreaslyn]

I think the following might be working:

let (evd, belowB) = EConstr.fresh_global (Global.env ()) !evd (ConstRef below) in

and then use this evd, if polymorphic.

There is another (maybe similar) problem in Splitting.define_tree. When invoking Obligations.add_mutual_definitions in

ignore(Obligations.add_mutual_definitions [(i, t', ty', impls, obls)] 
          (Evd.evar_universe_context !isevar) [] ~kind
            ~reduce ~hook (Obligations.IsFixpoint [recarg, CStructRec]))

I have tried to add debug statements in the hook:

let hook locality gr =
  let f = fst (Global.constr_of_global_in_context (Global.env ()) gr) in
  let () = Feedback.msg_debug (Printer.pr_constr f) in
  ...

The message was: f@{Var(0)}, which I think is wrong.

[mattam82]

I think the add_mutual is fine, but the "constr_of_global_in_context" is incorrect, however that is code you added, right?

I'm trying to build your branch now and see if I can fix the remaining issues.

[mattam82]

Maybe your build script is not up-to date actually, I get fatal: reference is not a tree: f895effe3f507e138c781134c621d76035c97e5f

[andreaslyn]

let f = fst (Global.constr_of_global_in_context env (ConstRef prog.program_cst)) in ...

is used in the bottom of Equations.define_principles, where I get the same behavior.

[andreaslyn]

I have updated the build script.

[mattam82]

Ok, i will look into that tomorrow. Le mar. 17 juil. 2018 à 18:30, Andreas Lynge notifications@github.com a écrit :

I have updated the build script.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/895#issuecomment-405645042, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARWDtFFp9RMb4giLWkUVEGzdoKrjGks5uHhEggaJpZM4PUtGC .

[andreaslyn]

Cool. After building HoTT you can reproduce with sh build.sh Ex, which will build Equations and try to build examples/Basics.v. Before building Equations, maybe you will need to make clean and then delete the generated Makefile.

[mattam82]

Ok. I could fix the universe error. Indeed this constr_of_global_in_context was badly used. It's now in the 8.8 branch. The next problem is that equations calls Indschemes.combined_scheme which looks for "and" and does not find it, it should be replaced by "prod". This commit should allow to progress: https://github.com/mattam82/coq/commit/95608597b78ed1b029cf2fb0731623616c5c2e25

[andreaslyn]

It seems that there is a problem with solving obligations on recursive definitions. For example:

Obligation Tactic := idtac.
Equations succ_not_zero (n:nat) : S n ≠ O :=
succ_not_zero O := HoTTUtil.nat_path_S_O ;
succ_not_zero (S n) :=
  let dummy := succ_not_zero n in _.

Solving the obligation with the following code works.

Next Obligation. intros f n dummy. exact HoTTUtil.nat_path_S_O. Defined.

But solving with

Next Obligation. intros f n dummy H. exact (HoTTUtil.nat_path_S_O H). Defined.

after Defined, it gives the error:

Illegal application: 
The term "succ_not_zero_obligation_1" of type
 "(∀ n : nat, n.+1 ≠ 0) → ∀ n : nat, n.+2 ≠ 0"
cannot be applied to the terms
 "succ_not_zero" : "∀ n : nat, n.+1 ≠ 0"
 "n0" : "nat"
The 1st term has type
 "forall n : nat, not@{Basics.18 Basics.18} (@paths@{Basics.18} nat (S n) O)"
which should be coercible to
 "forall n : nat, not@{Basics.21 Basics.21} (@paths@{Basics.21} nat (S n) O)".

The universes of succ_not_zero_obligation_1 change. Right before invoking Obligations.add_mutual_definitions in Splitting.define_tree, using Univops.universes_of_constr, I find that the only universe of succ_not_zero_obligation_1 is Basics.18. Later, right before the error message is printed, the only universe of succ_not_zero_obligation_1 is Basics.21.

I have not been able to reproduce this problem on nonrecursive definitions. The code can be found in file Basics.v in branch hott-port-debug.

[spitters]

@cmangin ? I believe that @mattam82 is not available

[cmangin]

I'm not sure this an Equations problem. Doing it just with Program like this:

Require Import HoTT.Basics.Overture.
Require Import Equations.HoTTUtil Program.Tactics.

Obligation Tactic := idtac.

Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) :=
match n as n return not (paths (S n) 0) with
| 0 => HoTTUtil.nat_path_S_O
| S n' => let dummy := succ_not_zero n' in _
end.
Next Obligation. intros f _ n dummy H. exact (HoTTUtil.nat_path_S_O H). Defined.

also fails, so it looks to me like an Obligations problem. I am by no means a universes expert though, maybe this is wrong. (Also I don't have a solution for now.)

[andreaslyn]

I think that Obligations.declare_obligation https://github.com/andreaslyn/coq/blob/e127e98cbb0bde822b338ae72369cad0b977728f/vernac/obligations.ml#L624 is being called with body and ty parameters having an unexpected set of universes. I have tried to add a hardcoded (u,Eq,v) constraint using Environ.add_constraints, which worked, but I'm not sure constraints is the way to go. For now I can circumvent the issue by commenting out the check in the kernel https://github.com/andreaslyn/coq/blob/e127e98cbb0bde822b338ae72369cad0b977728f/kernel/constr.ml#L787.

[andreaslyn]

The hott-port-debug branch can be used to reproduce the issue.

[mattam82]

@andreaslyn ok. I'm trying to reproduce

[mattam82]

The issue was indeed in Program Fixpoint in presence of polymorphic universes. Hopefully this can be backported to 8.8.2.

[spitters]

@mattam82 will this be backported into 8.8.2 ?

[andreaslyn]

@mattam82 I have merged my changes with the master branch in hott-port-master. This has indeed solved the obligations issue. Now I am getting

Conversion test raised an anomaly: Anomaly "Universe Top.1005 undefined."
Please report at http://coq.inria.fr/bugs/.

when running ./build.sh Ex.

[mattam82]

@spitters it was backported indeed

[mattam82]

Ok, I'm trying to reproduce

[mattam82]

I'm getting an error: "Error: cannot find Coq.Init.Logic.and; maybe library Coq.Init.Logic has to be required first."

when processing the first definition in Basics.v, because it tries to build a combined scheme calling a Coq function which expects and/conj to be defined in Init.Logic. How come you don't get that?

A PR fixing this in Coq, allowing to build combined schemes for principles in Type was just merged in Coq's master (might be in 8.9).

[mattam82]

Actually, even the obligation bug still happens. There must be something wrong with my installation. I see I'm using Coq's commit 063abf16b (for coq-HoTT), is that right?

[mattam82]

Hmm, apparently I was using an old version of hott-port-master, let me try again

[andreaslyn]

Deleting the custom-HoTT folder and running build.sh HoTT should give you the right version.

[mattam82]

Yes, but I had an issue with ./build.sh HoTT. Anyway, I get the error now.