Merge pull request #83 from math-comp/type-casts

Workaround for the type cast issue

examples/field_examples.v

@@ -34,6 +34,9 @@ Goal forall (F : fieldType) (n : nat),
     n%:R != 0 :> F -> (2 * n)%:R / n%:R = 2%:R :> F.
 Proof. by move=> F n n_neq0; field. Qed.
 
+Goal forall (F : fieldType) (x : F), x * 2%:R = (2%:R : F) * x.
+Proof. by move=> F x; field. Qed.
+
 (* For a numFieldType, non-nullity conditions such as 2%:R != 0 should not be *)
 (* generated.                                                                 *)
 Goal forall (F : numFieldType) (x : F), (x / 2%:R) * 2%:R = x.

examples/ring_examples.v

@@ -47,6 +47,9 @@ Proof. move=> H; ring: H. Qed.
 Goal (n.+1)%:R = n%:R + 1 :> R.
 Proof. ring. Qed.
 
+Goal a * 2%:R = (2%:R : R) * a.
+Proof. ring. Qed.
+
 End AbstractCommutativeRing.
 
 Section AbstractRingMorphism.

theories/lra.elpi

@@ -138,6 +138,7 @@ coqZ->Q tt (coqZneg P) {{ Qmake (-1) lp:P }} :- !.
 % [quote.nat In OutM Out] reifies natural number constant [In] of type [nat] to
 % a term [OutM] of type [large_nat] and [Out] of type [coqZ].
 pred quote.nat i:term, o:term, o:coqZ.
+quote.nat {{ lp:In : _ }} OutM Out :- !, quote.nat In OutM Out.
 quote.nat {{ Nat.of_num_uint lp:X }} {{ large_nat_uint lp:X }} Out :-
   ground-uint X, !,
   coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !,
@@ -148,6 +149,7 @@ quote.nat X {{ large_nat_N lp:XN }} Out :-
 % [quote.int In OutM Out] reifies integer constant [In] of type [int] to a term
 % [OutM] of type [large_int] and [Out] of type [coqZ].
 pred quote.int i:term, o:term, o:coqZ.
+quote.int {{ lp:In : _ }} OutM Out :- !, quote.int In OutM Out.
 quote.int {{ Posz (Nat.of_num_uint lp:X) }} {{ large_int_Pos lp:X }} Out :-
   ground-uint X, !,
   coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !, coqZ->N Out XN.
@@ -178,8 +180,8 @@ quote.int {{ Negz lp:N }} {{ large_int_Z (Zneg lp:P) }} (coqZneg P) :-
 pred quote.expr i:bool, i:term, i:option term, i:term, i:option term,
     i:(term -> term), i:term, o:term, o:term, o:list term.
 % _ : _
-quote.expr ff R F TR TUR Morph {{ lp:E : _ }} OutM Out VM :- !,
-  quote.expr ff R F TR TUR Morph E OutM Out VM.
+quote.expr ff R F TR TUR Morph {{ lp:In : _ }} OutM Out VM :- !,
+  quote.expr ff R F TR TUR Morph In OutM Out VM.
 % 0%R
 quote.expr _ R _ _ _ _ {{ @GRing.zero lp:U }}
            {{ @R0 lp:R }} {{ PEc (Qmake 0 1) }} _ :-

theories/ring.elpi

@@ -49,6 +49,7 @@ quote.expr.exp In1 In2 {{ @PEpow Z lp:In1 lp:In2 }} :- !.
 % [quote.ncstr In OutM Out] reifies natural number constant [In] of type [nat]
 % to a term [OutM] of type [large_nat] and a term [Out] of type [N].
 pred quote.ncstr i:term, o:term, o:term.
+quote.ncstr {{ lp:In : _ }} OutM Out :- !, quote.ncstr In OutM Out.
 quote.ncstr {{ Nat.of_num_uint lp:In }} {{ large_nat_uint lp:In }} Out :-
   ground-uint In, !,
   coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out.
@@ -57,6 +58,7 @@ quote.ncstr In {{ large_nat_N lp:Out }} Out :-
 
 % [quote.icstr In Pos OutM Out] reifies integer constant
 pred quote.icstr i:term, o:bool, o:term, o:term.
+quote.icstr {{ lp:In : _ }} Pos OutM Out :- !, quote.icstr In Pos OutM Out.
 quote.icstr {{ Posz (Nat.of_num_uint lp:In) }}
             tt {{ large_nat_uint lp:In }} Out :-
   ground-uint In, !,
@@ -77,6 +79,8 @@ quote.icstr In Pos {{ large_nat_N lp:Out }} Out :- !,
 % - [OutM] and [Out] are reified terms of [Input], and
 % - [VarMap] is a variable map.
 pred quote.nat i:term, i:term, o:term, o:term, o:list term.
+quote.nat R {{ lp:In : _ }} OutM Out VarMap :- !,
+  quote.nat R In OutM Out VarMap.
 quote.nat _ {{ lib:num.nat.O }} {{ NC (large_nat_N lib:num.N.N0) }} Out _ :- !,
   quote.expr.constant {{ lib:num.Z.Z0 }} Out.
 quote.nat R {{ lib:num.nat.S lp:In }} OutM Out VarMap :- !,
@@ -125,6 +129,9 @@ quote.count-succ In 0 In :- !.
 % - [VarMap] is a variable map.
 pred quote.zmod i:term, i:term, i:(term -> term), i:term,
                 o:term, o:term, o:list term.
+% _ : _
+quote.zmod U R Morph {{ lp:In : _ }} OutM Out VarMap :- !,
+  quote.zmod U R Morph In OutM Out VarMap.
 % 0%R
 quote.zmod U _ _ {{ @GRing.zero lp:U' }} {{ @ZM0 lp:U }} Out _ :-
   coq.unify-eq U U' ok, !,
@@ -182,6 +189,9 @@ quote.zmod _ _ _ In _ _ _ :- coq.error "Unknown" {coq.term->string In}.
 % - [VarMap] is a variable map.
 pred quote.ring i:term, i:option term, i:term, i:(term -> term),
                 i:term, o:term, o:term, o:list term.
+% _ : _
+quote.ring R F TR Morph {{ lp:In : _ }} OutM Out VarMap :- !,
+  quote.ring R F TR Morph In OutM Out VarMap.
 % 0%R
 quote.ring R _ _ _ {{ @GRing.zero lp:U }} {{ @R0 lp:R }} Out _ :-
   coq.unify-eq U {{ GRing.Ring.zmodType lp:R }} ok, !,