The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all, playing with coq terms, I was very surprised of the size of the
proof term when you use "inversion" tactic, compared to the one with a
simple manual trick.

>>>
Require Import BinPos.
Parameter ident: Type.
Parameter type_name: Type.
Parameter values: type_name -> Type.


Inductive type_stack: Type :=
| Bottom: type_stack
| Push: type_name -> type_stack -> type_stack
.
Notation "⊥" := (Bottom).
Notation "t ↓ s" := (Push t s) (right associativity, at level 20).

(** ** The stack index *)
Inductive stack_index (tn: type_name): type_stack -> Type :=
| Top: forall s, stack_index tn (Push tn s)
| Pop: forall s, stack_index tn s -> forall tn', stack_index tn (Push
tn' s) .

Inductive dep_type: type_stack -> Type :=
| Leaf: forall s, type_name -> dep_type s
| Dep : forall tn s, stack_index tn s -> values tn -> dep_type s ->
dep_type s | Prod: forall s, dep_type s -> dep_type s -> dep_type s
| Root: forall tn s, dep_type (Push tn s) -> dep_type s
.

Inductive value_stack: type_stack -> Type :=
| Vbottom: value_stack ⊥
| Vpush: forall tn, values tn ->
         forall s, value_stack s ->
         value_stack (tn↓s)
.

Fixpoint get_value1 (s: type_stack) tn (i: stack_index tn s)
: value_stack s -> values tn.
Proof.
 destruct i.
   intro H.
    clear get_value1.
    inversion H. (**)
    exact X.     (**)
   intro H.
    apply (get_value1 s tn i); clear i get_value1 tn.
    inversion H. (**)
    exact X0.    (**)
 Defined.

Fixpoint get_value2 (s: type_stack) tn (i: stack_index tn s)
: value_stack s -> values tn.
Proof.
 destruct i.
   intro H.
    clear get_value2.
(**)change (match tn↓s with ⊥ => (True:Type) | tn↓_ => values tn end).
(**)destruct H.
(**)  exact I.
(**)  exact v.
   intro H.
    apply (get_value2 s tn i); clear i get_value2 tn.
(**)change (match tn'↓s with ⊥ => (True:Type) | _↓s => value_stack s
end). (**)destruct H.
(**)  exact I.
(**)  exact H.
 Defined.

Print get_value1. (* 96 lines of output *)
Print get_value2. (* 35 lines of output *)

Notation "'invert_stack' t" :=
 (match t with Bottom => _ | _ ↓ _ => _ end) (at level 0, t ident).

(* get_value2 exploiting a notation to be of about 17 loc AND
   almost readable as I consider get_value1 to be unreadable *)

Definition get_value (tn: type_name) :=
fix get_value s (i : stack_index tn s): value_stack s -> values tn :=
  match i in (stack_index _ t0) return (value_stack t0 -> values tn)
with | Top s0 =>
      fun vs =>
      match vs in (value_stack t0) return invert_stack t0 with
      | Vbottom => I
      | Vpush _ v _ _ => v
      end
  | Pop s0 i0 tn' =>
      fun vs =>
      get_value s0 i0
        (match vs in value_stack t0 return invert_stack t0 with
         | Vbottom => I
         | Vpush _ _ _ vtn => vtn
         end)
  end.
<<<

Is there someone working on having such proof term generation?
I admit, that before doing my inversion I put my goal in a special form
(in fact I went the furthest as possible without requiring to use
inversion, so that using inversion will be done on the smallest type)

 I may be wrong, but I believe that there is no tactic doing this now.
If I am wrong, please tell it me, so my proofs will be a lot lighter
(I never use the manual trick I did here).

 If you think such a tactic would be cool, I would be glad to try to
implement it (I never programmed directly a tactic in OCaml).