uwplse / fix-to-elim Goto Github PK
View Code? Open in Web Editor NEWFixpoint to eliminator translation in Coq
License: MIT License
Fixpoint to eliminator translation in Coq
License: MIT License
The following:
From mathcomp Require Import tuple.
From Ornamental Require Import Ornaments.
Set DEVOID search prove equivalence. (* <-- Correctness proofs for search *)
Set DEVOID lift type. (* <-- Prettier types than the ones Coq infers *)
Module M.
Definition mytuple := cons_tuple.
End M.
Preprocess Module M as M'.
raises error:
Error:
Cannot find the elimination combinator tuple_of_rect, the elimination of the inductive definition tuple_of on sort
Type is probably not allowed.
But I can't find a way of makingtuple_of
opaque. I have tried:
Preprocess Module M as M' { opaque ssreflect.tuple.tuple_of }.
but it raises:
Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.
Even though ssreflect.tuple.tuple_of
is a qualified path in scope.
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.
The following is a little hard to minimize, so while I work on it, here is the somewhat long version:
From mathcomp Require Import seq.
From mathcomp Require Import ssreflect.
From mathcomp Require Import ssrfun.
From mathcomp Require Import ssrnat.
From mathcomp Require Import tuple.
From Ornamental Require Import Ornaments.
Set DEVOID search prove equivalence. (* <-- Correctness proofs for search *)
Set DEVOID lift type. (* <-- Prettier types than the ones Coq infers *)
Scheme Induction for tuple_of Sort Prop.
Scheme Induction for tuple_of Sort Set.
Scheme Induction for tuple_of Sort Type.
Scheme Induction for eqtype.Sub_spec Sort Prop.
Scheme Induction for eqtype.Sub_spec Sort Set.
Scheme Induction for eqtype.Sub_spec Sort Type.
Scheme Induction for eqtype.Equality.type Sort Prop.
Scheme Induction for eqtype.Equality.type Sort Set.
Scheme Induction for eqtype.Equality.type Sort Type.
Scheme Induction for eqtype.Equality.mixin_of Sort Prop.
Scheme Induction for eqtype.Equality.mixin_of Sort Set.
Scheme Induction for eqtype.Equality.mixin_of Sort Type.
Scheme Induction for eqtype.subType Sort Prop.
Scheme Induction for eqtype.subType Sort Set.
Scheme Induction for eqtype.subType Sort Type.
Module Bits.
Definition BITS n := n.-tuple bool.
Definition joinlsb {n} (pair: BITS n*bool) : BITS n.+1 := cons_tuple pair.2 pair.1.
Fixpoint fromNat {n} m : BITS n :=
if n is _.+1
then joinlsb (fromNat m./2, odd m)
else nil_tuple _.
Definition toNat {n} (p: BITS n) := foldr (fun (b:bool) n => b + n.*2) 0 p.
Definition adcB {n} (carry : bool) (p1 p2: BITS n) := p1. (* splitmsb (adcBmain carry p1 p2). *)
End Bits.
Module Helper.
Definition joinLSB {n} (v : Vector.t bool n) (lsb : bool) : Vector.t bool n.+1 :=
Vector.shiftin lsb v.
Fixpoint bvNat (size : nat) (number : nat) : Vector.t bool size :=
if size is size'.+1
then joinLSB (bvNat size' (number./2)) (Nat.odd number)
else Vector.nil _
.
Fixpoint bvToNat (size : nat) (v : Vector.t bool size) : nat :=
Vector.fold_left (fun n (b : bool) => b + n.*2) 0 v.
End Helper.
Module M.
Definition bitvector : forall (n : nat), Type := (fun (n : nat) => Vector.t bool n).
Axiom bvult : forall (n : nat), (((@M.bitvector) (n))) -> (((@M.bitvector) (n))) -> bool.
Definition bvCarry : forall (n : nat), (((@M.bitvector) (n))) -> (((M.bitvector) (n))) -> bool :=
(fun (n : nat) (x : Vector.t bool n) (y : Vector.t bool n) =>
((@M.bvult) (n) (Helper.bvNat _ (Bits.toNat (((@Bits.adcB) (n) false (Bits.fromNat (Helper.bvToNat _ x)) (Bits.fromNat (Helper.bvToNat _ y)))))) (x))).
End M.
Preprocess Module M as M'
{ opaque
M.bvult
mathcomp.ssreflect.ssrnat.half
}.
The pre-processing fails with error:
Error: Illegal application (Non-functional construction):
The expression "n0" of type "nat" cannot be applied to the term
"n1" : "nat"
The following code:
From Coq Require Import Vectors.Vector.
Module V.
Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
Fixpoint atWithDefault (n : nat) (a : Type) (default : a) (v : Vec n a) (index : nat)
: a
:=
match v with
| Vector.nil _ => default
| Vector.cons _ h n' t =>
match index with
| O => h
| S index' => atWithDefault n' _ default t index'
end
end
.
End V.
Preprocess Module V as V'.
fails with error:
Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/.
The following, however, succeeds:
From Coq Require Import Vectors.Vector.
Module V.
Fixpoint atWithDefault (n : nat) (a : Type) (default : a) (v : Vector.t a n) (index : nat)
: a
:=
match v with
| Vector.nil _ => default
| Vector.cons _ h n' t =>
match index with
| O => h
| S index' => atWithDefault n' _ default t index'
end
end
.
End V.
Preprocess Module V as V'.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.