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 [email protected] 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 [email protected] 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 [email protected] 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 [email protected] 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.