Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Induction on lemma proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Induction on lemma proof


Chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Induction on lemma proof
  • Date: Fri, 15 Mar 2013 14:53:56 +0100

Hi,

If you want do try an induction on the list e, you should not
introduce too much variables as in your proof start:
intros e j (h1,h2) n h3.

Just try:

Proof.
induction e.

Then look at the generated goals (empty list, list obtained by consing
some value of type or_integer_float to a list e0).
In the last case, you may have a look at the induction hypothesis on e0.

Then you have a lot of things to do : Instantiate (if needed) some universally
quantified hypotheses, case analysis on type or_integer_float, destruct the
conjonctions in your axioms, etc.

By the way, which libraries do you use on lists ? Standard Library's List ?

Pierre






Quoting
mtkhan AT risc.uni-linz.ac.at:

Hi All,

I have a Coq goal, which is in fact translated from Why3 system.
I tried the induction on list but could not succeed. Can some
one please hint the possible proof tactics in Coq for the
following snippet of the corresponding proof.

...
Parameter add_int: (list or_integer_float) -> Z -> Z.
...
Axiom add_int_def : forall (e:(list or_integer_float)) (j:Z),
((j <= 0%Z)%Z -> ((add_int e j) = 0%Z)) /\ ((~ (j <= 0%Z)%Z) ->
((add_int e j) = match e with
| Nil => 0%Z
| (Cons (Integer n) t) => (n + (add_int t (j - 1%Z)%Z))%Z
| (Cons _ t) => (add_int t (j - 1%Z)%Z)
end)).

(* Why3 goal *)
Theorem add_int_right : forall (e:(list or_integer_float)) (j:Z),
((0%Z <= j)%Z /\ (j < (length e))%Z) -> forall (n:Z), ((nth j
e) = (Some (Integer n))) -> ((add_int e (j + 1%Z)%Z) = ((add_int e
j) + n)%Z).
intros e j (h1,h2) n h3.

which shows the following 1 goal to be proved

1 subgoal
e : list or_integer_float
j : Z
h1 : (0 <= j)%Z
h2 : (j < length e)%Z
n : Z
h3 : nth j e = Some (Integer n)
______________________________________(1/1)
add_int e (j + 1) = (add_int e j + n)%Z


Thanks.

regards,
tk







Archive powered by MHonArc 2.6.18.

Top of Page