search

uwplse / fix-to-elim

Fixpoint to eliminator translation in Coq
MIT License
3 stars 5 forks source link

Failure to preprocess Coq.ZArith.BinInt #11

Closed Ptival closed 4 years ago

Ptival commented 4 years ago

The following:

From Coq Require Import ZArith.BinInt.

Scheme Induction for Coq.Classes.CRelationClasses.StrictOrder Sort Prop.
Scheme Induction for Coq.Classes.CRelationClasses.StrictOrder Sort Set.
Scheme Induction for Coq.Classes.CRelationClasses.StrictOrder Sort Type.

Preprocess Module Coq.ZArith.BinInt as BinInt'.

results in the error:

Coq_ZArith_BinInt_Z_add_diag is defined
Coq_ZArith_BinInt_Z_mul_1_l is defined
Coq_ZArith_BinInt_Z_one_succ is defined
Coq_Init_Nat_add is defined
Coq_ZArith_BinInt_Pos2Z_inj_iff is defined
Coq_Init_Logic_iff_sym is defined
Coq_ZArith_BinInt_Pos2Z_inj is defined
Coq_ZArith_BinInt_Z_mul_sub_distr_l is defined
Coq_ZArith_BinInt_Z_mul_add_distr_l is defined
Coq_ZArith_BinInt_Z_mul_opp_r is defined
Coq_ZArith_BinInt_Z_mul_opp_l is defined
Coq_ZArith_BinInt_Z_add_opp_diag_l is defined
Coq_ZArith_BinInt_Z_add_move_0_r is defined
Coq_ZArith_BinInt_Z_mul_eq_0_l is defined
Coq_ZArith_BinInt_Z_eq_mul_0 is defined
Coq_ZArith_BinInt_Z_mul_eq_0 is defined
Coq_ZArith_BinInt_Z_mul_pos_pos is defined
Coq_ZArith_BinInt_Z_mul_pos_neg is defined
Coq_ZArith_BinInt_Z_mul_neg_pos is defined
Coq_ZArith_BinInt_Z_mul_neg_neg is defined
Coq_ZArith_BinInt_Z_lt_neq is defined
Coq_ZArith_BinInt_Z_lt is defined
Coq_ZArith_BinInt_Z_lt_trichotomy is defined
Coq_ZArith_BinInt_Z_mul_lt_mono_pos_r is defined
Coq_ZArith_BinInt_Z_mul_lt_mono_pos_l is defined
Coq_ZArith_BinInt_Z_add_lt_mono is defined
Coq_ZArith_BinInt_Z_lt_ind is defined
Coq_ZArith_BinInt_Z_mul_lt_mono_neg_r is defined
Coq_ZArith_BinInt_Z_mul_lt_mono_neg_l is defined
Coq_ZArith_BinInt_Z_mul_comm is defined
Coq_ZArith_BinInt_Z_mul_lt_pred is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_lt_trans is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_not_ge_lt is defined
Coq_ZArith_BinInt_Z_le_lt_add_lt is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_le_lt_trans is defined
Coq_ZArith_BinInt_Z_lt_succ_l is defined
Coq_Classes_Morphisms_Prop_all_iff_morphism is defined
Coq_ZArith_BinInt_Z_order_induction_0 is defined
Coq_ZArith_BinInt_Z_add_lt_mono_r is defined
Coq_ZArith_BinInt_Z_add_lt_mono_l is defined
Coq_ZArith_BinInt_Z_add_le_mono is defined
Coq_ZArith_BinInt_Z_nlt_ge is defined
Coq_ZArith_BinInt_Z_add_le_mono_l is defined
Coq_ZArith_BinInt_Z_add_le_mono_r is defined
Coq_ZArith_BinInt_Z_le_trans is defined
Coq_ZArith_BinInt_Z_succ_le_mono is defined
Coq_ZArith_BinInt_Z_succ_lt_mono is defined
Coq_Classes_Morphisms_Prop_all_iff_morphism_obligation_1 is defined
Coq_Init_Logic_all is defined
Coq_Classes_Morphisms_pointwise_relation is defined
Coq_ZArith_BinInt_Z_order_induction is defined
Coq_ZArith_BinInt_Z_right_induction is defined
Coq_ZArith_BinInt_Z_left_induction is defined
Coq_ZArith_BinInt_Z_rs_rs' is defined
Coq_ZArith_BinInt_Z_strong_right_induction is defined
Coq_ZArith_BinInt_Z_lt_exists_pred is defined
Coq_ZArith_BinInt_Z_lt_exists_pred_strong is defined
Coq_ZArith_BinInt_Z_le_le_succ_r is defined
Coq_ZArith_BinInt_Z_le_succ_r is defined
Coq_ZArith_BinInt_Z_rs'_rs'' is defined
Coq_ZArith_BinInt_Z_rbase is defined
Coq_ZArith_BinInt_Z_A'A_right is defined
Coq_ZArith_BinInt_Z_lt_lt_succ_r is defined
Coq_ZArith_BinInt_Z_ls_ls' is defined
Coq_ZArith_BinInt_Z_strong_left_induction is defined
Coq_ZArith_BinInt_Z_ls'_ls'' is defined
Coq_ZArith_BinInt_Z_lbase is defined
Coq_ZArith_BinInt_Z_A'A_left is defined
Coq_ZArith_BinInt_Z_le_ngt is defined
Coq_ZArith_BinInt_Z_eq_le_incl is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_lt_eq is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_not_gt_le is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_IsTotal_lt_total is defined
Coq_ZArith_BinInt_Z_mul_succ_r is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_eq_sym is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_eq_lt is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_lt_irrefl is defined
Coq_ZArith_BinInt_Z_Private_OrderTac_Tac_trans is defined
Error: Illegal application: 
The term "StrictOrder_ind" of type
 "forall (A : Type) (R : CRelationClasses.crelation A) (P : CRelationClasses.StrictOrder R -> Prop),
  (forall (StrictOrder_Irreflexive : CRelationClasses.Irreflexive R)
     (StrictOrder_Transitive : CRelationClasses.Transitive R),
   P
     {|
     CRelationClasses.StrictOrder_Irreflexive := StrictOrder_Irreflexive;
     CRelationClasses.StrictOrder_Transitive := StrictOrder_Transitive |}) ->
  forall s : CRelationClasses.StrictOrder R, P s"
cannot be applied to the terms
 "A" : "Type"
 "R" : "Relation_Definitions.relation A"
 "RelationClasses.Transitive R" : "Prop"
 "fun (_ : RelationClasses.Irreflexive R) (StrictOrder_Transitive : RelationClasses.Transitive R) =>
  StrictOrder_Transitive"
   : "RelationClasses.Irreflexive R -> RelationClasses.Transitive R -> RelationClasses.Transitive R"
 "StrictOrder" : "RelationClasses.StrictOrder R"
The 3rd term has type "Prop" which should be coercible to "CRelationClasses.StrictOrder R -> Prop".

The code in CRelationClasses is universe-polymorphic, which does not seem to be supported, so this might be a cause for the trouble. Not sure how to work around this.

tlringer commented 4 years ago

Oh yeah, basically zero plugins support universe polymorphism :/

tlringer commented 4 years ago

But I'm not sure if that's the particular issue here. I'll take a look.

tlringer commented 4 years ago

When you run this the first time, what definition does it say that it is working on before you hit this error?

Ptival commented 4 years ago

When I run the Preprocess command on existing Coq modules, the Transforming <term> messages don't seem to be emitted.

e.g.

Preprocess Module Coq.Init.Datatypes as Datatypes'.
tlringer commented 4 years ago

I do see the output for those, which is why I find it confusing. In CoqIDE they show up. Can you try running it via coqc on command line?

tlringer commented 4 years ago

Though it does not print it for dependencies it pulls in, which is a bug I need to fix

Ptival commented 4 years ago 
[...]
Transforming identity
Transforming identity_rect
Transforming identity_ind
Transforming identity_rec
Transforming ID
Transforming id
Transforming IDProp
Transforming idProp
[error here]
tlringer commented 4 years ago

I pushed better reporting that prints when it transforming dependencies, too. The last message before the error is:

Transforming dependency Coq.Classes.RelationClasses.StrictOrder_Transitive

I will look into why this fails and whether we need to work around it or fix it in the plugin.

tlringer commented 4 years ago

Full function definition is:

RelationClasses.StrictOrder_Transitive = 
fun (A : Type) (R : Relation_Definitions.relation A)
  (StrictOrder : @RelationClasses.StrictOrder A R) =>
match StrictOrder return (@RelationClasses.Transitive A R) with
| RelationClasses.Build_StrictOrder _ _ StrictOrder_Transitive =>
    StrictOrder_Transitive
end
tlringer commented 4 years ago

For now, you can run it with the following opaque definitions (of course this can cause problems if you want to lift them in DEVOID later, and may mean that you need to make things that depend on them opaque later too):

Preprocess Module Coq.ZArith.BinInt as BinInt' 
  { opaque
      Coq.Classes.RelationClasses.StrictOrder_Transitive 
      Coq.Classes.RelationClasses.StrictOrder_Irreflexive
      Coq.Classes.RelationClasses.Equivalence_Transitive
      Coq.Classes.RelationClasses.Equivalence_Reflexive
      Coq.Classes.RelationClasses.Equivalence_Symmetric
      Coq.Classes.RelationClasses.PER_Symmetric
      Coq.Classes.RelationClasses.PER_Transitive
      Coq.PArith.BinPos.Pos.add_reg_r
      Coq.PArith.BinPos.Pos.add_no_neutral
      Coq.PArith.BinPos.Pos.compare_sub_mask
      Coq.PArith.BinPos.Pos.sub_mask_carry_spec
      Coq.PArith.BinPos.Pos.sub_mask_carry
      Coq.PArith.BinPos.Pos.add_carry
      Coq.PArith.BinPos.Pos.sub_mask
      Coq.PArith.BinPos.Pos.peano_rect
      Coq.PArith.BinPos.Pos.add
  }.

I will look at the particular definitions and try to figure out why this is happening. Some of them are mutual recursion, but some of them like StrictOrder_Transitive I just don't know.

tlringer commented 4 years ago

Ah, the root cause seems to be that Scheme induction defines induction principles that look different from the ones that Coq defines for inductive types in Prop more generally. So when you generate induction schema for Prop, you should write:

Scheme Minimality for Coq.Classes.RelationClasses.StrictOrder Sort Prop.

The following thus works:

From Coq Require Import ZArith.BinInt.

Scheme Minimality for Coq.Classes.RelationClasses.StrictOrder Sort Prop.
Scheme Induction for Coq.Classes.RelationClasses.StrictOrder Sort Set.
Scheme Induction for Coq.Classes.RelationClasses.StrictOrder Sort Type.

Scheme Minimality for Coq.Classes.RelationClasses.Equivalence Sort Prop.

Scheme Minimality for Coq.Classes.RelationClasses.PER Sort Prop.

Preprocess Module Coq.ZArith.BinInt as BinInt'
  { opaque
      Coq.PArith.BinPos.Pos.add_reg_r 
      Coq.PArith.BinPos.Pos.add_no_neutral
      Coq.PArith.BinPos.Pos.compare_sub_mask 
      Coq.PArith.BinPos.Pos.sub_mask_carry_spec 
      Coq.PArith.BinPos.Pos.sub_mask_carry 
      Coq.PArith.BinPos.Pos.add_carry 
      Coq.PArith.BinPos.Pos.sub_mask 
      Coq.PArith.BinPos.Pos.peano_rect 
      Coq.PArith.BinPos.Pos.add
  }.

The rest appear to be mutual recursion.

I unfortunately don't know how to provide good error messaging for this.

tlringer commented 4 years ago

Updated the README and added much better error messaging for all of these situations.