SSReflect and Math Components in HoTT

[andreaslyn]

I have a HoTT branch https://github.com/andreaslyn/HoTT/tree/ssr with support for all the basic ssreflect tactics. The goal is to be able to build math components with HoTT and hopefully without changing code in math components. @mattam82 @amahboubi do you have ideas on how to do this?

Changes to make SSReflect Coq files compile

A few changes to the basic ssreflect files are needed. The following Coq compatibility file SSRPreamble.v is imported by all the 4 basic ssreflect Coq files:

Require Export HoTT.Basics.Overture HoTT.Types.Bool.

Global Unset Asymmetric Patterns.

Notation "{ A } + { B }" := (A + B) (at level 50, left associativity).
Notation "A + { B }" := (A + B) (at level 50, left associativity).
Notation "A \/ B" := (A + B).

Notation sym_equal := @inverse.
Notation eq := paths.
Notation proj1 := fst.
Notation proj2 := snd.
Notation projT1 := @proj1_sig.
Notation left := inl.
Notation inleft := inl.
Notation or := sum.
Notation bool := Bool.
Notation unit := Unit.
Notation refl_equal := @idpath.
Notation sym_eq := @inverse.
Notation sym_not_eq := @symmetric_neq.
Notation trans_eq := @concat.
Notation f_equal := @ap.

Definition f_equal2 (A1 A2 B : Type) (f : A1 -> A2 -> B)
  (x1 y1 : A1) (x2 y2 : A2) (p1 : x1 = y1) (p2 : x2 = y2)
  : f x1 x2 = f y1 y2
  := match ap f p1 in _ = g return f x1 x2 = g y2 with
     | idpath => ap (f x1) p2
     end.

Delimit Scope bool_scope with bool.

The remaining changes are:

• Change Prop everywhere to Type.
• Replace #[universes(template)] with Cumulative. Note that simply removing #[universes(template)] seems to work as well.
• The proofs of all_tag2 and all_sig2 in ssrfun.v need to change the use of all_pair to @all_pair I. I don't know why this needs to be changed.
• In ssrbool.v the type of if_spec is changed from Set to Type, which is needed because of changing Prop to Type.
• In ssreflect.v the UNDER_EQ and UNDER_IFF module types need some explicit universe annotations, because of universe polymorphism.

When PR https://github.com/coq/coq/pull/10457 has been merged into Coq, then the above lists all the changes to the basic ssreflect Coq files required to compile them with HoTT.

Changes to math components

It may also be feasible to build math components with HoTT. Similar issues occur when attempting to do so:

• Change Prop everywhere to Type.
• Add additional definitions to SSRPreamble.v.
• Inside module types, some parts need explicit universe annotations.
• Notation issues, e.g. the == notation is homotopy in HoTT and equality in math components.
• Seemingly arbitrary expressions need to be modified slightly to work. For example ssreflect/eqtype.v in math components, the proof of SubP need to apply rec explicitly: case: sT Sub_spec SubSpec u => /= U _ mkU rec _. apply: rec., where the proof working in coq is: by case: sT Sub_spec SubSpec u => /= U _ mkU rec _.
• In ssreflect/eqtype.v in math components: tag_eq = eq_op is a type error (need to provide the canonical structure explicitly for some reason tag_eq = @eq_op tag_eqType), but sum_eq = eq_op works just fine.

[amahboubi]

Hi @andreaslyn ! Sorry for the late comment. I will unfortunately not have any time to review this anytime before September, as I am leaving office now for a summer break. But may be @CohenCyril or @gares will have feedback before I am back online.

[andreaslyn]

The following two branches allows one to play with ssreflect in HoTT:

• https://github.com/andreaslyn/HoTT/tree/SSR-THIS-ONE
• https://github.com/andreaslyn/coq/tree/SSR-FOR-HoTT

Maybe someone will be interested in continuing this.

[gares]

Thanks @andreaslyn I gave a quick look and at least some of the commit were proposed as PR in Coq's repo. Are you saying there are more commits I should pick from the Coq tree?

[andreaslyn]

@gares I made those changes to the Coq sources to make ssreflect work in HoTT. Maybe some of those things have been fixed already in Coq, so I am not sure how much of it needs to be merged.