Stream: Coq users

Topic: Simpl/ ssreflect and cbv iota fail to simplify a fixpoint


view this post on Zulip walker (Oct 23 2022 at 21:05):

I couldn't reproduce a smaller poc of the issue I am facing but here it is:

From Coq Require Import PArith.

Inductive TNode (A: Type) : Type :=
| TNode001: TNode A -> TNode A
| TNode010: A -> TNode A
| TNode011: A -> TNode A -> TNode A
| TNode100: TNode A -> TNode A
| TNode101: TNode A -> TNode A ->TNode A
| TNode110: TNode A -> A -> TNode A
| TNode111: TNode A -> A -> TNode A -> TNode A.
Arguments TNode001 {A} _.
Arguments TNode010 {A} _.
Arguments TNode011 {A} _ _.
Arguments TNode100 {A} _.
Arguments TNode101 {A} _ _.
Arguments TNode110 {A} _ _.
Arguments TNode111 {A} _ _ _.

Inductive Trie (A: Type): Type :=
| Tempty : Trie A
| Troot: TNode A -> Trie A.
Arguments Tempty {A}.
Arguments Troot {A} _.

Definition trie_builder {A} (l: Trie A) (o: option A) (r: Trie A) : Trie A :=
match l,o,r with
| Tempty, None, Tempty => Tempty
| Tempty, None, Troot r' => Troot (TNode001 r')
| Tempty, Some x, Tempty => Troot (TNode010 x)
| Tempty, Some x, Troot r' => Troot (TNode011 x r')
| Troot l', None, Tempty => Troot (TNode100 l')
| Troot l', None, Troot r' => Troot (TNode101 l' r')
| Troot l', Some x, Tempty => Troot (TNode110 l' x)
| Troot l', Some x, Troot r' => Troot (TNode111 l' x r')
end.
Global Arguments trie_builder: simpl never.

Fixpoint tnode_singleton {A} (p: positive) (a: A) :=
 match p with
| xH => TNode010 a
| xO q => TNode100 (tnode_singleton q a)
| xI q => TNode001 (tnode_singleton q a)
end.

Definition trie_singleton {A} (p: positive) (a: A) := Troot (tnode_singleton p a).
Global Arguments trie_singleton: simpl never.

Fixpoint trie_alter {A} (t: Trie A) (f: option A -> option A) (p: positive)  : Trie A :=
match t with
| Tempty => match f None with
            | None => Tempty
            | Some a => trie_singleton p a
            end
| Troot n =>
    match p, n with
    | xH, TNode001 r => trie_builder Tempty (f None) (Troot r)
    | xH, TNode010 a => trie_builder Tempty (f (Some a)) Tempty
    | xH, TNode011 a r => trie_builder Tempty (f (Some a)) (Troot r)
    | xH, TNode100 l => trie_builder (Troot l) (f None) Tempty
    | xH, TNode101 l r => trie_builder (Troot l) (f None) (Troot r)
    | xH, TNode110 l a => trie_builder (Troot l) (f (Some a)) Tempty
    | xH, TNode111 l a r => trie_builder (Troot l) (f (Some a)) (Troot r)
    | xO q, TNode001 r => trie_builder (trie_alter Tempty f q ) None (Troot r)
    | xO q, TNode010 a => trie_builder (trie_alter Tempty f q ) (Some a) Tempty
    | xO q, TNode011 a r => trie_builder (trie_alter Tempty f q) (Some a) (Troot r)
    | xO q, TNode100 l => trie_builder (trie_alter (Troot l) f q) None Tempty
    | xO q, TNode101 l r => trie_builder (trie_alter (Troot l) f q) None (Troot r)
    | xO q, TNode110 l y => trie_builder (trie_alter (Troot l) f q) (Some y) Tempty
    | xO q, TNode111 l y r => trie_builder (trie_alter (Troot l) f q) (Some y) (Troot r)
    | xI q, TNode001 r => trie_builder Tempty None (trie_alter (Troot r) f q )
    | xI q, TNode010 a => trie_builder Tempty (Some a) (trie_alter Tempty f q)
    | xI q, TNode011 a r => trie_builder Tempty (Some a) (trie_alter (Troot r) f q)
    | xI q, TNode100 l => trie_builder (Troot l) None (trie_alter Tempty f q )
    | xI q, TNode101 l r => trie_builder (Troot l) None (trie_alter (Troot r) f q )
    | xI q, TNode110 l a => trie_builder (Troot l) (Some a) (trie_alter Tempty f q )
    | xI q, TNode111 l a r => trie_builder (Troot l) (Some a) (trie_alter (Troot r) f q )
    end
end.
Arguments trie_alter _ !_/_ _.  (*This line does not really matter, I tried to force unfolding*)
Lemma foo: forall A g p, g None = None -> trie_alter (@ Tempty A) g p  = Tempty.
Proof.
intros. simpl.
Admitted.

This code is me playing with binary trie implementation but that is not the point.

The simpl should have replaced trie_alter (@ Tempty A) g p with

match f None with
            | None => Tempty
            | Some a => trie_singleton p a
            end

part of the trie_alter function.

but that never happened, I tried various simplifying tactics including cbv and it never reduced to the match statement. It is not clear why.

view this post on Zulip Gaëtan Gilbert (Oct 23 2022 at 21:19):

the recursive argument of the fix is p so it won't reduce when given a variable for it

view this post on Zulip walker (Oct 23 2022 at 21:31):

wait it looks for me that the recursive argument it t , it is the thing always decreasing, no ?

view this post on Zulip Gaëtan Gilbert (Oct 23 2022 at 21:40):

try making it explicit with {struct t} and see what happens

view this post on Zulip walker (Oct 23 2022 at 21:49):

yup, that requires a bit of rewriting to get {struct t} happy


Last updated: Jan 31 2023 at 14:03 UTC