Illegal application (Non-functional construction)

[Ptival]

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"

[tlringer]

Did we figure this out yesterday?

[Ptival]

We did.

We had to add Nat.even to the opaque list, because it does recursion on its input minus two.

[tlringer]

Oh right, so action item for me is detecting n-induction for n > 1 and messaging the user