The Coq mailing list

[Igor Jirkov <igorjirkov AT gmail.com>]

Hello!

I have a problem trying to prove a property of form:

forall (n:nat) (m:T),  n > s m -> f (g n m) = f n.

Here f: T -> U , g: nat -> T -> T , s: T -> nat.

The problem is that g  is defined as a fixpoint with decreasing n, I presume that it obliges me to use the proof by induction.

However, induction over n  is giving me premises I can not satisfy:

(n > s m -> f (g n m) = f n) -> (S n > s m -> f (g n m) ).

Having (S n > s m) I can not deduce  (n > s m).

Are there some recipes to cope with that kind of proofs?

** The description below lists  a bit more code in case it might help; however, it bases on the CompCert's implementation of PTrees (Patricia Trees) so I can not shape a minimal working example **

The property I want to prove is stated as this:

Fixpoint map_last_index {T} (m:Maps.PTree.t T) route :=
  match m with
  | Node Leaf _ Leaf => route
  | Node Leaf _ r => (map_last_index r route) ~1
  | Node l  _ Leaf => (map_last_index l route) ~0                                  
  | Node l _ r => max ((map_last_index  l route)~0) ((map_last_index r route)~1)
  | Leaf => 1
  end.

Fixpoint map_remove_r {T} (idx:nat) (m:Maps.PTree.t T) ( rem_at: positive)
   : Maps.PTree.t T :=
      (match compare (of_nat idx) rem_at, get (of_nat idx) m with
      | Lt, Some e => set (of_nat idx) e
      | Gt, Some e => set ((of_nat idx)-1) e
      | _, _ => fun x => x
      end
      )
        match idx with
        | 0%nat => Leaf
        | S n => map_remove_r n m rem_at
end.

Theorem spec_r:
  forall T (m:Maps.PTree.t T) b1 b0 n,
    (b1 < b0)%positive ->
    n > to_nat (map_last_index m 1) ->
    get b1 ( map_remove_r n m b0) = get b1 m.

map_remove  removes an element from a tree by index and shifts all next elements so that they are stored on an index equal to their old position minus one, filling the
"gap".

The node in a binary tree is located using  binary numbers to encode the route from the root. They serve as indices.

map_last_index computes the last index  a tree has a node for.

BR

Igor Zhirkov