wip

elpi/constraints/constraint-graph.elpi

@@ -114,18 +114,19 @@ maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained v
 
 % assign a constant class to a variable and update all the information in the graph
 % indeed, if the assigned variable was an output class for complex constraints,
-% they can now be computed and reduced to simpler constraints on the other variables
+% they can now be computed and   reduced to simpler constraints on the other variables
 pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph.
 instantiate ID Class G _ :-
   util.when-debug dbg.steps (coq.say "instantiate" ID Class G), fail.
 instantiate ID Class (constraint-graph G) (constraint-graph G') :-
-  std.map.find ID G (pr LowerNodes HigherNodes), !,
+  std.map.find ID G (pr LowerNodes HigherNodes), !, std.do! [
   internal.filter-var LowerNodes LowerIDs,
   util.unless (LowerIDs = [])
     (coq.error
       "wrong instantiation order: trying to instantiate" ID "before lower variables" LowerIDs),
   std.fold HigherNodes G (instantiate.aux ID Class) G1,
-  std.map.remove ID G1 G'.
+  std.map.remove ID G1 G'
+  ].
 instantiate ID Class G G :-
   util.when-debug dbg.full (
     coq.say "cannot instantiate" ID "at" Class "because it is not in the graph").
@@ -135,27 +136,30 @@ instantiate.aux ID Class (node.const C) G G :-
   util.unless (param-class.geq C Class)
     (coq.error
       "constraint not respected: instantiating" ID "at class" Class "despite upper bound" C).
-instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :-
+instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- std.do![
   util.map.update IDA (internal.remove-lower-node (node.var ct.pi [ID])) G G1,
   util.map.update IDB (internal.remove-lower-node (node.var ct.pi [ID])) G1 G2,
   % recompute the dependent product constraint and turn it into 2 order constraints
   param-class.dep-pi Class C1 C2,
   util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3,
-  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'.
-instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :-
+  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'
+].
+instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- std.do![
   util.map.update IDA (internal.remove-lower-node (node.var ct.arrow [ID])) G G1,
   util.map.update IDB (internal.remove-lower-node (node.var ct.arrow [ID])) G1 G2,
   % recompute the arrow type constraint and turn it into 2 order constraints
   param-class.dep-arrow Class C1 C2,
   util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3,
-  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'.
-instantiate.aux ID Class (node.var ct.type [IDR]) G G' :-
+  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'
+].
+instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- std.do![
   util.map.update IDR (internal.remove-lower-node (node.var ct.type [ID])) G G1,
   % the constraint either vanishes or forces the relation to be (4,4)
   if (param-class.requires-axiom Class)
     (util.map.update IDR (internal.add-lower-node (node.const (pc map4 map4))) G1 G')
-    (G' = G1).
-instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :-
+    (G' = G1)
+].
+instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- std.do! [
   std.fold {std.filter IDs (id\ id > 0)} G (id\ g\ g'\
     util.map.update id (internal.remove-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g')
       G1,
@@ -164,7 +168,8 @@ instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :-
   trocq.db.gref GR Class Cs GR' GRR, !,
   coq.env.global GR' Tm',
   % make sure the classes are consistent
-  instantiate.gref IDs TCs Cs G1 G'.
+  instantiate.gref IDs TCs Cs G1 G'
+  ].
 pred instantiate.gref
   i:list class-id, i:list param-class, i:list param-class, i:constraint-graph-content,
   o:constraint-graph-content.
@@ -174,12 +179,13 @@ instantiate.gref [-1|IDs] [TC|TCs] [C|Cs] G G' :- !,
   % we just check that it is equal to the required one
   TC = C,
   instantiate.gref IDs TCs Cs G G'.
-instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :-
+instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- std.do![
   % here the identifier is not -1, which means that the class at this position is in the graph
   % we force it to be equal to C in the graph
   util.map.update ID (internal.add-lower-node (node.const C)) G G1,
   util.map.update ID (internal.add-higher-node (node.const C)) G1 G2,
-  instantiate.gref IDs TCs Cs G2 G'.
+  instantiate.gref IDs TCs Cs G2 G'
+].
 instantiate.aux ID Class (node.var ct.geq [IDH]) G G' :-
   % an order constraint is turned into a lower constant class
   util.map.update IDH (internal.remove-lower-node (node.var ct.geq [ID])) G G1,

elpi/constraints/constraints.elpi

@@ -118,7 +118,7 @@ pred c.vars? o:list class-id.
 pred c.vars! o:list class-id.
 
 pred vars? o:list class-id.
-vars? IDs :- !, std.spy(declare_constraint (c.vars? IDs) [_]).
+vars? IDs :- !, declare_constraint (c.vars? IDs) [_].
 pred vars! i:list class-id.
 vars! IDs :- !, declare_constraint (c.vars! IDs) [_].
 
@@ -216,7 +216,7 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra
     cstr-graph.add-geq IDorC1 IDorC2 G G',
     declare_constraint (c.graph G') [_]
   ).
-  rule \ (c.graph G) (c.reduce-graph) <=> (std.spy-do! [
+  rule \ (c.graph G) (c.reduce-graph) <=> (std.do! [
     coq.say "final constraint graph START:",
     vars? IDs,
     util.when-debug dbg.full (
@@ -240,17 +240,18 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra
 % return a list of associations of a variable and its constant class
 pred reduce i:list class-id, i:constraint-graph, o:list (pair class-id param-class).
 reduce [] _ [].
-reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :-
+reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- std.do! [
   cstr-graph.minimal-class ID ConstraintGraph MinClass,
   util.when-debug dbg.full (coq.say "min value" MinClass "for" ID),
   cstr-graph.maximal-class ID ConstraintGraph MaxClass,
   util.when-debug dbg.full (coq.say "max value" MaxClass "for" ID),
   util.unless (param-class.geq MaxClass MinClass) (coq.error "no solution for variable" ID),
-  reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues.
+  reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues
+].
 
 % now instantiate for real
 pred instantiate-coq i:pair class-id param-class.
-instantiate-coq (pr ID (pc M0 N0)) :- std.spy-do! [
+instantiate-coq (pr ID (pc M0 N0)) :- std.do! [
   util.when-debug dbg.full (coq.say "instantiating" ID "with" (pc M0 N0)),
   link- C ID,
   univ-link- C M N,

elpi/param.elpi

@@ -133,19 +133,17 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
 param
   (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N])
   (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :-
-    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.spy-do! [
+    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do! [
       util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" M N),
       cstr.univ-link C M N,
       util.when-debug dbg.full (coq.say "param/arrow:" M N "is linked to" C),
       cstr.dep-arrow C CA CB,
       util.when-debug dbg.full (coq.say "param/arrow: added dep-arrow from" C "to" CA "and" CB),
       cstr.univ-link CA MA NA,
       util.when-debug dbg.full (coq.say "param/arrow:" MA NA "is linked to" CA),
-      % std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
-      % if (TyA = sort prop)
-      %   (PTypeA = app [pglobal (const {trocq.db.pprop}) _, M1A, M2A])
-      %   (PTypeA = app [pglobal (const {trocq.db.ptype}) _, M1A, M2A]),
-      PTypeA = (app [pglobal (const PType) _, MA, NA]),
+      std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
+      if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA),
+      PTypeA = (app [pglobal (const PTypeGRA) _, MA, NA]),
       param A PTypeA A' AR,
       cstr.univ-link CB MB NB,
       util.when-debug dbg.full (coq.say "param/arrow:" MB NB "is linked to" CB),
@@ -170,7 +168,7 @@ param
 param
   (prod N A B) (app [pglobal (const PType) _, M1, M2])
   (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :-
-    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.spy-do![
+    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![
     util.when-debug dbg.steps (coq.say "param/forall" N ":" A "," B "@" M1 M2),
     coq.name-suffix N "'" N',
     coq.name-suffix N "R" NR,
@@ -180,15 +178,13 @@ param
     util.when-debug dbg.full (coq.say "param/forall: added dep-pi from" C "to" CA "and" CB),
     cstr.univ-link CA M1A M2A, !,
     util.when-debug dbg.full (coq.say "param/forall:" M1A M2A "is linked to" CA),
-    % std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
-    % if (TyA = sort prop)
-    %   (PTypeA = app [pglobal (const {trocq.db.pprop}) _, M1A, M2A])
-    %   (PTypeA = app [pglobal (const {trocq.db.ptype}) _, M1A, M2A]),
-    PTypeA = (app [pglobal (const PType) _, M1A, M2A]),
+    std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
+    if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA),
+    PTypeA = (app [pglobal (const PTypeGRA) _, M1A, M2A]),
     param A PTypeA A' AR,
     cstr.univ-link CB M1B M2B, !,
     util.when-debug dbg.full (coq.say "param/forall:" M1B M2B "is linked to" CB),
-    @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.spy-do![
+    @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.do![
       util.when-debug dbg.full (coq.say "param/forall: introducing" a "@" A "~" a' "by" aR),
       param (B a) (app [pglobal (const PType) _, M1B, M2B]) (B' a') (BR a a' aR), !,
       util.when-debug dbg.full (coq.say "param/forall:" (B a) "@" M1B M2B "~" (B' a') "by" (BR a a' aR))

examples/Vector_tuple.v

@@ -11,7 +11,7 @@
 (*                            * see LICENSE file for the text of the license *)
 (*****************************************************************************)
 
-From Coq Require Import ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrnat.
 From Trocq Require Import Trocq.
 From Trocq Require Import Param_nat Param_trans Param_bool Param_vector.
 
@@ -23,7 +23,7 @@ Definition tuple (A : Type) : nat -> Type :=
   fix F n :=
     match n with
     | O => Unit
-    | S n' => F n' * A
+    | S n' => (F n' * A)%type
     end.
 
 Definition const : forall {A : Type} (a : A) (n : nat), tuple A n :=
@@ -77,7 +77,7 @@ Definition vector_to_tupleK {A : Type} :
     fix F n v :=
       match v with
       | Vector.nil => idpath
-      | Vector.cons m a v' => ap (Vector.cons a) (F m v')
+      | Vector.cons _ a v' => ap (Vector.cons a) (F _ v')
       end.
 
 Definition tuple_to_vectorK {A : Type} :
@@ -215,7 +215,7 @@ Trocq Use Param_append Param_const Param01_paths.
 Lemma append_const : forall {A : Type} (a : A) (n1 n2 : nat),
   append (const a n1) (const a n2) = const a (n1 + n2).
 Proof.
-  trocq. exact @Vector.append_const.
+  trocq; exact: @Vector.append_const.
 Qed.
 
 End AppendConst.
@@ -279,10 +279,11 @@ Proof. by trocq. Qed.
 (* bounded nat and bitvector *)
 (* NB: we can use transitivity to make the proofs here too *)
 
+
 Module BV.
 
-Definition bounded_nat (k : nat) := {n : nat & n < pow 2 k}%nat.
-Definition bitvector (k : nat) := Vector.t Bool k.
+Definition bounded_nat (k : nat) := {n : nat & n < expn 2 n = true}%nat.
+Definition bitvector := (Vector.t Bool).
 
 (* bounded_nat k ~ bitvector k' *)
 
@@ -314,33 +315,24 @@ Lemma S_add1 : forall (n : nat), S n = (n + 1)%nat.
 Proof.
   induction n.
   - simpl. reflexivity.
-  - simpl add. apply ap. exact IHn.
+  - by rewrite addn1.
 Defined.
 
-Lemma one_lt_pow2 (k : nat) : (1 <= pow 2 k)%nat.
+Lemma one_lt_pow2 (k : nat) : (1 <= expn 2 k)%nat = true.
 Proof.
+Search expn (leq 1).
   induction k.
-  - simpl. apply leq_n.
-  - apply (leq_trans IHk).
-    simpl.
-    apply n_leq_add_n_k.
-Defined.
+  - simpl.
+Admitted.
 
 Axiom bv_bound :
-  forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= pow 2 k - 1)%nat.
+  forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= expn 2 k - 1)%nat = true.
 
 Definition bv_to_bnat {k : nat} (bv : bitvector k) : bounded_nat k.
 Proof.
   unshelve econstructor.
   - exact (bv_to_nat bv).
-  - apply (mixed_trans1 _ (pow 2 k - 1) _).
-    * apply bv_bound.
-    * apply natpmswap1.
-      1: { apply one_lt_pow2. }
-      rewrite nat_add_comm.
-      rewrite <- (S_add1 (pow 2 k)).
-      apply n_lt_Sn.
-Defined.
+Admitted.
 
 Axiom map_in_R_bv_bnat :
   forall {k : nat} {bv : bitvector k} {bn : bounded_nat k},
@@ -386,7 +378,7 @@ Definition Param44_bnat_bv (k k' : nat) (kR : natR k k') :
   Param44.Rel (bounded_nat k) (bitvector k').
 Proof.
   unshelve eapply (@Param44_trans _ (bitvector k) _).
-  - exact Param44_bnat_bv_d.
+  - exact Param44_bnat_bv_d.  
   - exact (Vector.Param44 Bool Bool Param44_Bool k k' kR).
 Defined.
 
@@ -425,22 +417,21 @@ Axiom getBitR :
     (n n' : nat) (nR : natR n n'),
       BoolR (getBit_bnat bn n) (getBit_bv bv' n').
 
-(* lt ~ lt *)
-Axiom Param10_lt :
+Axiom Param10_le :
   forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'),
-    Param10.Rel (n1 < n2)%nat (n1' < n2')%nat.
+    BoolR (n1 <= n2)%nat (n1' <= n2')%nat.
 
 Axiom setBitThenGetSame :
   forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool),
-    (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b.
+    (i < k)%nat = true -> getBit_bv (setBit_bv bv i b) i = b.
 
 
 Trocq Use Param2a0_nat Param44_Bool Param2a0_bnat_bv getBitR setBitR.
-Trocq Use Param01_paths Param10_lt.
+Trocq Use Param01_paths Param10_paths Param10_le trueR SR.
 
 Lemma setBitThenGetSame' :
   forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool),
-    (i < k)%nat -> getBit_bnat (setBit_bnat bn i b) i = b.
+    (i < k)%nat = true -> getBit_bnat (setBit_bnat bn i b) i = b.
 Proof.
   trocq. exact @setBitThenGetSame.
 Qed.

examples/flt3_step.v

@@ -71,7 +71,7 @@ Notation "x ≡ y" := (eqmodp x%int y%int)
   (format "x  ≡  y", at level 70) : int_scope.
 Notation "x ≢ y" := (not (eqmodp x%int y%int))
   (format "x  ≢  y", at level 70) : int_scope.
-Notation "x ≠ y" := (not (x = y)).
+Notation "x ≠ y" := (not (x = y)) (at level 70).
 Notation "ℤ/9ℤ" := Zmod9.
 Notation ℤ := int.
 
@@ -88,7 +88,9 @@ Variable Reqmodp01 : forall (m : int) (x : Zmod9), Rp m x ->
 
 
 Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01.
-Trocq Use Param01_sum Param01_Empty Param10_Empty.
+Trocq Use Param01_sum.
+Trocq Use Param01_Empty.
+Trocq Use Param10_Empty.
 
 Lemma flt3_step : forall (m n p : ℤ),
   m * n * p % 3 ≢ 0 -> (m³ + n³)%ℤ  ≠ p³%ℤ.

examples/int_to_Zp.v

@@ -27,20 +27,6 @@ rewrite modNz_nat// val_Zp_nat//= /Zp_trunc/=.
 rewrite modnS.
 case: ifP.
   rewrite subn0 modnn.
-(*   
-  rewrite subn1.
-rewrite -[n.+1]addn1.
-rewrite modnD//=.
-rewrite modnS /dvdn.
-rewrite modn_small//; last first.
-  rewrite ltn_psubLR//. leq_addl//.
-Search (_ - _ < _)%N.
-Search (_.+1 %% _)%N.
-
-Search (_ %% _)%Z (_ %% _)%N.
-rewrite val_Zp
-congr Posz.
- rewrite val_Zp_nat//.  *)
 Admitted.
 
 Lemma Zp_int_mod [p : nat] : 1 < p ->
@@ -126,42 +112,15 @@ Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01 RTrue Runit.
 
 Local Open Scope ring_scope.
 
-Lemma IntRedModZp : int -> True.
- (* (forall (m n : 'Z_p), m = n * n -> m = 0) ->
- forall (m n : int),  eqmodp m n. *)
+Lemma IntRedModZp : 
+ (forall (m n : 'Z_p), m = n * n -> m = n) ->
+ forall (m n : int),  m = int_mul n n -> eqmodp m n.
 Proof.
-(* move=> Hyp. *)
+move=> Hyp.
 trocq; simpl.
 exact: Hyp.
 Qed.
 
 (* Print Assumptions IntRedModZp. (* No Univalence *) *)
 
-End IntToZmod7.
-
-Module Zmod7ToInt.
-
-Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK).
-
-Axiom Rzero : Rp zerop zero.
-Variable Radd : binop_param Rp Rp Rp addp add.
-Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp.
-
-Trocq Use Rp Param01_paths Param10_paths Radd Rzero.
-
-Goal (forall x y, x + y = y + x)%Zmod7.
-Proof.
-  trocq.
-  exact addC.
-Qed.
-
-Goal (forall x y z, x + y + z = y + x + z)%Zmod7.
-Proof.
-  intros x y z.
-  suff addpC: forall x y, (x + y = y + x)%Zmod7. {
-    by rewrite (addpC x y). }
-  trocq.
-  exact addC.
-Qed.
-
-End Zmod7ToInt.
+End modp.