The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I know that the "omega" tactic can solve inequalities over Z.

  Suppose now, I have defined my own class, as follows:

Inductive Expr :=

  | eVar (s: string)

  | eAdd (e1 e2: Expr)

  | eSub (e1 e2: Expr).

Inductive myProp :=

  | mLe (e1 e2: Expr)

  | mLt (e1 e2: Expr)

  | mEq (e1 e2: Expr)

Fixpoint expr_denote (env: Env) (expr: Expr) :=

  match expr with

    | eVar s => env_lookup env s (* returns a Z *)

    | eAdd e1 e2 => (expr_denote env e1) + (expr_denote env e2)

    | eSub e1 e2 => (expr_denote env e1) - (expr_denote env e2)

  end.

Definition prop_denote (env: Env) (prop: myProp) :-

  match prop with

    | mLe e1 e2 => (expr_denote env e1) <= (expr_denote env e2)

    | mLt e1 e2 => (expr_denote env e1) < (expr_denote env e2)

    | mEq e1 e2 => (expr_denote env e1) = (expr_denote env e2)

  end.

Lemma lem1:

  forall env e1 e2 e3 e4,

    prop_denote env (mLe e1 e2) ->
    prop_denote env (mLe e2 e3) ->
    prop_denote env (mLe (eAdd e1 e4) (eAdd e3 e4)).

Now, is there some way to:

(*) prove some basic facts about prop_denote expr_denote

(*) NOT unfold prop_denote expr_denote

(*) prove lem1 via "omega"-like, where "omega"-like is operating on the level of expressions, rather than unfolding everything into Z's and reasoning about Z's

Thanks!