probleme mit verifun

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

komme beim verifizieren von 'nat2byte is injective' einfach nicht mehr weiter. das ist der zielterm:

Code: Alles auswählen

if{even(x1),
  if{-(x1) = -(y1), true, ¬ even(-(-(y1)))},
  if{-(x1) = -(y1), true, even(-(-(y1)))}}
die hypothesen sind:
* half(x1) = half(y1)
* ?+(-(-(y1)))
* ?+(x1)

warum es funktionieren muss ist klar, aber ich finde kein handliches lemma um das ganze zu beweisen

---

das lemma: wenn x ungleich y und even_x = even_y dann half_x = half_y, dass ich zum beweisen formuliert hatte, hängt im wesentlichen an der gleichen stelle
We can do this the hard way or my way ...which is basically the same thing!

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Beitrag von Gnomix »

Code: Alles auswählen

if{?⁺(y1),
  if{?⁺(x1),
    if{half(x1) = half(y1),
      if{even(x1),
        if{⁻(x1) = ⁻(y1), true, ¬ even(y1)},
        if{⁻(x1) = ⁻(y1), true, even(y1)}},
      true},
    true},
  true}
Also ich kann mich Baerchen nur anschließen.
Bei mir hängt er sich am selben Schritt auf.
Er "vereinfacht" zwar noch einmal, aber das Ergebnis ist noch komplizierter.

Code: Alles auswählen

if{?⁺(x1),
  if{?⁺(⁻(⁻(y1))),
    if{half(x1) = half(⁻(⁻(y1))),
      true,
      if{half(x1) = ⁺(half(⁻(⁻(y1)))),
        if{even(x1),
          if{⁻(x1) = ⁻(y1), true, ¬ even(⁻(⁻(y1)))},
          if{⁻(x1) = ⁻(y1), true, even(⁻(⁻(y1)))}},
        true}},
    if{⁻(x1) = ⁻(y1), true, if{even(x1), ¬ half(x1) = 1, true}}},
  true}

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Beitrag von Christoph Walther »

Gnomix hat geschrieben:

Code: Alles auswählen

if{?succ(y1),
  if{?succ(x1),
    if{half(x1) = half(y1),
      if{even(x1),
        if{pred(x1) = pred(y1), true, ¬ even(y1)},
        if{pred(x1) = pred(y1), true, even(y1)}},
      true},
    true},
  true}
Also ich kann mich Baerchen nur anschließen.
Bei mir hängt er sich am selben Schritt auf.
Angenommen, 'half' ist injektiv. Mit 'half(x1) = half(y1)' gilt dann auch 'x1 = y1'. Da x1 und y1 ungleich 0 sind, gilt dann auch 'pred(x1) = pred(y1)' und wir sind fertig. Leider ist 'half' aber nicht injektiv (lemma 'half is injektiv' mit dem Disprover widerlegen lassen). Warum? Wenn man die antwort darauf hat, dann kann man damit ein lemma formulieren, das zwar schwächer als die injektivität von 'half' ist, aber immer noch so stark ist, daß der beweis gelingt.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

saß schon die ganze zeit daran genau so ein schwächeres injektivitätskriterium zu formalieren. habe es jetzt in zwei lemmata aufgeteilt, jeweils eins für den fall das x gerade und eins für den fall dass x ungerade. beide lemmata grün, beweis von nat2byte neu angeschmissen und innerhalb von 5 sekunden grün. das leben ist schön :)
We can do this the hard way or my way ...which is basically the same thing!

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Beitrag von Gnomix »

Christoph Walther hat geschrieben: Angenommen, 'half' ist injektiv. Mit 'half(x1) = half(y1)' gilt dann auch 'x1 = y1'. Da x1 und y1 ungleich 0 sind, gilt dann auch 'pred(x1) = pred(y1)' und wir sind fertig. Leider ist 'half' aber nicht injektiv (lemma 'half is injektiv' mit dem Disprover widerlegen lassen). Warum? Wenn man die antwort darauf hat, dann kann man damit ein lemma formulieren, das zwar schwächer als die injektivität von 'half' ist, aber immer noch so stark ist, daß der beweis gelingt.
Sehe ich das richtig, dass half(x) und half(x+1) das selbe ergeben, wenn x gerade ist ?
Und wir also zeigen müssen, dass wenn even(x)=even(y) und half(x)=half(y) dann auch x=y ?
Ich hänge nämlich noch immer an der selben Stelle und komme nicht vorran.

Apropos, euch allen einen guten Rutsch und ein frohes neues Jahr.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

das sieht doch ganz gut aus :)
We can do this the hard way or my way ...which is basically the same thing!

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: probleme mit verifun

Beitrag von Gnomix »

Hmm, also ich habe jetzt ein weiteres Lemma gefunden, dass meinen Beweisbaum von zwei offenen Zweigen auf einen reduziert.
Allerdings bleibe ich an folgender Aussage hängen:

Code: Alles auswählen

if{⁻(⁻(x1)) = ⁻(⁻(y1)),
  true,
  if{even(⁻(⁻(x1))),
    true,
    if{even(⁻(⁻(y1))),
      true,
      if{?⁺(⁻(⁻(x1))),
        if{⁻(⁻(⁻(x1))) = half(⁻(⁻(y1))),
          if{even(⁺(half(⁻(⁻(x1))))),
            true,
            ¬ nat2byte(half(⁺(half(⁻(⁻(x1))))))
              = nat2byte(half(⁺(half(⁻(⁻(y1))))))},
          if{even(⁺(half(⁻(⁻(y1))))),
            if{even(⁺(half(⁻(⁻(x1))))),
              ¬ nat2byte(half(⁺(half(⁻(⁻(x1))))))
                = nat2byte(half(⁺(half(⁻(⁻(y1)))))),
              true},
            if{even(⁺(half(⁻(⁻(x1))))),
              true,
              ¬ nat2byte(half(⁺(half(⁻(⁻(x1))))))
                = nat2byte(half(⁺(half(⁻(⁻(y1))))))}}},
        ¬ ?0(⁻(⁻(⁻(y1))))}}}}
Wenn ich ein paar Schritte weiter hoch gehe sehe ich , dass diese Aussage aus der folgenden folgt:

Code: Alles auswählen

if{?⁺(y1),
  if{?⁺(x1),
    if{⁻(x1) = ⁻(y1),
      true,
      if{even(x1),
        true,
        if{even(y1), true, ¬ nat2byte(half(x1)) = nat2byte(half(y1))}}},
    true},
  true}
Irgendwie stehe ich hier auf dem Schlauch.
Hat vielleicht noch jemand noch einen Tipp für mich.

Benutzeravatar
Maradatscha
Computerversteher
Computerversteher
Beiträge: 353
Registriert: 2. Okt 2006 18:53

Re: probleme mit verifun

Beitrag von Maradatscha »

so wie ich das sehe funktioniert bei dir alles bis auf den noteven Fall
hast du für den noteven Fall schon bewiesen dass half injektiv ist?

Pyron
Windoof-User
Windoof-User
Beiträge: 36
Registriert: 17. Dez 2005 17:15
Wohnort: Darmstadt

Re: probleme mit verifun

Beitrag von Pyron »

Hallo,

ich weiß zwar, dass es recht knapp ist bis Donnerstag, aber ich habe sehr lange gebraucht zu verstehen wie denn nun Verifun wirklich funktioniert ;)
Also der Beweis von "byte-add is correct" ist endlich grün und nun wollte ich mich an byte-mult heranmachen.

Nun zum eigentlichen Problem. Wenn ich "byte-mult" rechtsklicke, kann ich "Change Procedure" nicht auswählen. Ich habe also "Change Depending" ausgewählt, und die Funktion soweit verändert wie beschrieben, also die Sterne durch Implementierungen ersetzt.

Allerdings schneidet Verifun nun einige Sachen ab, wenn ich auf OK klicke. Diverse Delta/Dreieck-Mults, die wohl unterfunktionen waren.
Wenn ich im Interpreter die byte-mult Funktion teste, scheint alles ganz normal zu sein, also es fällt nicht auf, dass irgendwas weggeschnitten wurde.

Aber ist es denn so gewollt? Oder fehlen mir nun zum Beweisen von "byte-mult is correct" irgendwelche Unterfunktionen die byte-mult brauch?
Ich werde nun erstmal auf verdacht weitermachen und hoffe, dass es nicht weiter schlimm ist oder mir mehr Probleme bereitet als gedacht.


Ich habe es auch bei Verifun auf den Pool-Rechnern ausprobiert, dort kann ich bei "byte-add" ganz normal "change procedure" auswählen, aber bei byte-mult ist es die selbe Geschichte wie auf dem Laptop. "Change procedure" ist nicht auswählbar und man kann nur "change depending" und "modify depending" auswählen.

Vielen Dank für die evtl. Hilfe ;)

mfg

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: probleme mit verifun

Beitrag von aderhold »

Pyron hat geschrieben:Wenn ich "byte-mult" rechtsklicke, kann ich "Change Procedure" nicht auswählen. Ich habe also "Change Depending" ausgewählt, und die Funktion soweit verändert wie beschrieben, also die Sterne durch Implementierungen ersetzt.
Das ist richtig so, weil "byte-mult" schon von anderen (systemgenerierten) Objekten verwendet wird. Diese Objekte (Prozeduren und Lemmas) werden bei Bedarf automatisch wiederhergestellt (d. h. neu erzeugt). Durch diese Änderung geht also nichts verloren, was man später vermissen würde.

Pyron
Windoof-User
Windoof-User
Beiträge: 36
Registriert: 17. Dez 2005 17:15
Wohnort: Darmstadt

Re: probleme mit verifun

Beitrag von Pyron »

Vielen Dank für die schnelle Antwort :)

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: probleme mit verifun

Beitrag von Gnomix »

@Maradatscha: Genau das wars. Ich hatte nur für den Fall even(x) das Lemma gehabt.

Antworten

Zurück zu „Archiv“