uwplse / fix-to-elim Goto Github PK

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'.

Error:
Cannot find the elimination combinator tuple_of_rect, the elimination of the inductive definition tuple_of on sort
Type is probably not allowed.

Preprocess Module M as M' { opaque ssreflect.tuple.tuple_of }.

Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.

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'.

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".

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
       }.

Error: Illegal application (Non-functional construction): 
The expression "n0" of type "nat" cannot be applied to the term
 "n1" : "nat"

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'.

Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/.

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'.