The Coq mailing list

[Igor Jirkov <igorjirkov AT gmail.com>]

Hello everyone,

I have a problem with case-analysis on a term. This term is match'ed, and it is also used inside a type in one of the term's branches.

Here is a pseudocode to better illustrate the idea:

Hyp :  match <expr> as x return x = <expr> -> res with

    | Some n => fun Heq : Some n = <expr> => somefun Heq   (* usually an obligation generated by Program *)

    | _ => ...

end eq_refl

I think the problem is that an abstracted term (which is constructed internally during rewrites/destructs) is ill-typed. I have little idea about what can I do to make case-analysis on <expr>. 

What are the available techniques to cope with that?

I made a distilled MWE which shows the problem; the latest goal can be easily proved by induction on `n` ; however, in my actual code, the `expr` corresponds to getting an element from a tree-map and constraints are harder, so I really would like to make a case-analysis on the whole _expression_.

Definition sprev (e: nat) : option nat :=
  match e with
  | S n => Some n 
  | 0 => None
  end.

Record pos := mkpos { n: nat ; proof : exists z, sprev n = Some z } .

Definition is_some {T} (x: option T)  := match x with | Some _ => True | None => False end .

Definition build_pos n (H: is_some (sprev n) ) : pos .
  {
  unfold is_some in *.
  destruct (sprev n) eqn: Hf.
  eapply mkpos.
  exists n0; eauto. inversion H.
  } Defined.

Program Definition one := mkpos 1 _.
Next Obligation.  exists 0.   reflexivity. Defined.

Program Definition prev e  :=
  match sprev e with
  | Some (S m) =>  build_pos (S m) _
  | _ =>   one
  end.
Next Obligation. { intros. unfold is_some. subst. compute in Heq_anonymous. destruct e; inversion Heq_anonymous. subst. compute; auto. } Defined.
Solve All Obligations using discriminate.
 

(* in a minimal example it is easier to prove it by case analysis on `n`, but in a real program I need to do a case analysis on `sprev n` *)
Goal forall n, prev n = one -> n = 0 \/ n = 1 \/ n = 2.
  intros n H.
  unfold prev in H.
  destruct n. left; reflexivity.
  right.
  destruct n0. left; reflexivity.
  right.
  destruct n0.
  reflexivity. discriminate.
Abort.