[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Please Help Me



I managed to prove it using the prelude lemma "lub_nat" to get
at the largest natural less than j where the train is safe, and
measure-induct+ so that the induction works from i+1 to i.  I'm
making no claims that it is the best proof, but here it is:

(""
 (grind :if-match nil)
 (lemma "lub_nat")
 (inst -1 "{i | i < j!1 AND train!1(i) = safe}" "j!1")
 (("1"
   (grind :if-match nil)
   (inst 1 "n!1")
   (assert)
   (case "FORALL (k: upto(j!1)): n!1 < k IMPLIES train!1(k) = approaching")
   (("1" (skosimp) (inst -1 "m!1") (assert))
    ("2"
     (hide 2)
     (measure-induct+ "j!1 - k" ("k"))
     (inst -1 "x!1 + 1")
     (("1" (assert) (inst -8 "x!1") (assert) (inst -5 "x!1") (assert))
      ("2" (assert))))))
  ("2" (grind))))

Note that using measure-induct+ directly on the original
formula leads to an unprovable TCC; this is due to the
heuristics used by measure-induct+ to create the induction
formula.  The case step just provides an alternative equivalent
form that works.

Sam


> I can not prove the following lemma.
> 
> This THEORY is a part of railload crossing.
> 
> ===========
> 
> test: THEORY
> BEGIN
> 
> train_state: TYPE = { safe, approaching, crossing}
> Train: TYPE = [ nat -> train_state ]
> train: VAR Train
> i, j, k, m: VAR nat
> 
> 
> test_lemma: LEMMA
> (FORALL i: train(i+1) = approaching IMPLIES
>   train(i) = approaching OR train(i) = safe) AND
> train(0) = safe AND
> train(j) = approaching
> 
> IMPLIES
> 
>   (EXISTS k:
>     k < j AND train(k) = safe AND
>     (FORALL m:
>       k < m AND m <= j IMPLIES
>         train(m) = approaching ))
> 
> END test
> 
> ===========
> 
> 
> Would you mind please telling me about this?
> 
> 
> Kanazawa Univ ,Japan
> YAMAZAKI Takashi
>