Edit: The lemma below is incorrect and therefore not provable :). This `N.to_nat (N.div np 256 + 1)`

should be

`N.to_nat (log256 np + 1)`

, but it contains some useful information; hence I am not deleting this thread.

I am trying to rewrite an assumption into the goal, but getting this error:

```
Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
"and": ill-formed elimination predicate.
Theorem length_correctness : forall np : N, List.length (length_byte_list np) = N.to_nat (N.div np 256 + 1).
Proof.
intro np.
induction (N.lt_wf 0 np) as [up Hacc IHup].
refine(match (up <? 256) as upp return _ = upp -> _ with
| true => fun Hnp => _
| false => fun Hnp => _
end eq_refl).
+ apply N.ltb_lt in Hnp.
assert (Hup : up/256 = 0).
rewrite N.div_small;
[reflexivity | exact Hnp].
rewrite Hup.
unfold length_byte_list.
simpl. apply N.ltb_lt in Hnp.
(* rewrite Hnp is not working
which is ill-typed.
Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
"and": ill-formed elimination predicate. *)
admit.
```

Based on my (limited) understanding, it might be the case that this rewrite is creating some inconsistent state and therefore now allowing the rewrite, so my question is: how can I solve this? Complete source code [1]

[1] https://gist.github.com/mukeshtiwari/eb3376d4eb568628205d5b3469b85785

(0) Instead of a dependently typed "refine (match...)", what about `destruct (up <? 256) eqn:?`

(1) Can you poat the complete goal at the point of the error?

(2) I haven't seen this specific type error, but if rewrite is producing an ill-typed state because of dependent types, often one needs to actually understand the details of the type error, and change the state to fix it.

That might sound tautological, but this is one of the few scenario where one needs to typecheck a tactic output on their own to fix it!

(in fact, when using lots of dependent types, some prefer writing proof terms directly, so that it's easier to reason about them; see Agda)

(0) I changed it to `destruct (up <? 256) eqn:?`

but the error is same.

(1) I posted the error message on gist [1].

[1] https://gist.github.com/mukeshtiwari/82d56ffdce8e9707cb2c9baf610608b6

This goal is too unwieldy for this to be solvable in general (but ways out exist); my advice about using abstract to hide obligations was exactly to avoid having proof obligations inside your Defined terms.

however, I suspect I spotted the _first_ problem, tho I’m not sure if the usual workarounds would scale here

Now wrapping some terms into `abstract`

changed the error:

```
which is ill-typed.
Reason is: Illegal application:
The term "length_byte_list_subproof" of type
"∀ up : N, (up <? 256) = true → up < 256"
cannot be applied to the terms
"up" : "N"
"Hnp0" : "b = true"
The 2nd term has type "b = true" which should be coercible to
"(up <? 256) = true".
```

Here’s an extract of the first error:

```
Abstracting over the term "up <? 256" leads to a term
λ b : bool,
length
((if b as upp return (b = upp → list byte)
then
λ Hnp0 : b = true,
(np_total up (match N.ltb_lt up 256 with
| conj H _ => H
end Hnp0) :: Datatypes.nil)%list
…
which is ill-typed.
```

here, we cannot apply `N.ltb_lt up 256`

(or its first half) to `Hnp0 : b = true`

— even if we could apply it to `Hnp0 : up <? 256 = true`

.

So, rewriting `up <? 256`

in all occurrences is not possible directly.

your error is also of a similar kind

one basic idea is to (1) avoid rewriting in those positions where that causes a type error (2) trying to make that easier to scale.

Here, probably you can generalize over the proof term (`(match N.ltb_lt up 256 with | conj H _ => H end Hnp0)`

, or `length_byte_list_subproof up Hnp0`

) — it often doesn’t matter which exact proof you have that `up < 256`

.

alternatively, you can list the occurrences where to `rewrite`

.

Neither one scales so well with goal size, but `abstract`

might help already a bit.

Thansk @Paolo Giarrusso I don't know how to abstract the third bullet. I might look more into tomorrow (going for dinner). Enjoy your day!

```
Definition length_byte_list (np : N) : list byte.
Proof.
refine ((fix length_byte_list up (H: Acc (fun x y => (* 0 <= *) x < y) (N.div up 256)) {struct H} :=
match (up <? 256) as upp return _ = upp -> _ with
| true => fun Hnp => List.cons (np_total up _) List.nil
| false => fun Hnp =>
let r := N.modulo up 256 in
let t := N.div up 256 in
List.cons (np_total r _) (length_byte_list t _)
end eq_refl
) np (N_Lt_wf _)). (* ((@Acc_intro_generator _ (fun x y => 0 <= x < y) 100 (N.lt_wf 0)) (N.div np 256))). *)
+ abstract (apply N.ltb_lt in Hnp; exact Hnp).
+ abstract (apply (nmod_256 up)).
+ apply Acc_inv with (x := t). subst t; exact H.
apply N.ltb_ge in Hnp;
eapply N_eq_gt with (up := up); auto.
Show Proof.
Defined.
```

(deleted)

Mukesh Tiwari has marked this topic as resolved.

Last updated: Jul 24 2024 at 13:02 UTC