tło

Uczę się pomocy, Coq, na własną rękę. Do tej pory w pośpiechu przeczytałem Coq Yvesa Bertota . Teraz moim celem jest udowodnienie podstawowych wyników dotyczących liczb naturalnych, których zwieńczeniem jest tak zwany algorytm podziału. Jednak na drodze do tego celu napotkałem pewne niepowodzenia. W szczególności dwa następujące wyniki okazały się (gra słów zamierzona) trudniejsze do udowodnienia w Coq, niż początkowo sobie wyobrażałem. W rzeczywistości, po wielu bezowocnych próbach, postanowiłem je udowodnić ręcznie (jak pokazano poniżej). To najwyraźniej nie pomaga mi w opanowaniu Coq; dlatego zwracam się do tego forum. Mam nadzieję, że ktoś na tej stronie jest w stanie i chceaby pomóc mi przetłumaczyć poniższe dowody na dowód, który akceptuje Coq. Wszelka pomoc jest szczerze doceniana!

Twierdzenie A

Dla wszystkich $x,y \in N$

Przypuszczać $x < S(y)$. Stąd jest$z \in N$ z

Zdefiniuj predykat

Wystarczy pokazać $Q(z)$. Udowadniamy to przez włączenie indukcyjne$z$. Zobaczyć$Q(0)$, nie etat, jeśli $\text{I}(N,x+0,y)$ trzyma się wtedy $\text{I}(N,x,y)$jest zgodne z Peano 1a. A zatem,$x<y \lor \text{I}(n,x,y)$. Teraz udowodnimy$Q(S(v))$: Załóżmy $\text{I}(N,x+S(v),y)$. Z tej definicji mamy$x<y$ a zatem $x<y \lor \text{I}(N,x,y)$także w tym przypadku. Na koniec podaje piąty aksjomat Peano$Q(z)$ i przez $(*)$ dostajemy $x < y \lor \text{I}(N,x,y)$.

Twierdzenie B

Dla wszystkich $x,y \in N$

Gdyby $x<y$ następnie $\neg \text{I}(N,x,y)$ z definicji i jeśli $x>y$ następnie $\neg \text{I}(N,x,y)$również z definicji. Gdyby$x>y$ i $y>x$ potem mamy przechodniość i refleksyjność $\text{I}(N,x,y)$, co jest sprzecznością. W związku z tym nie więcej niż jedno ze stwierdzeń jest prawdziwe.

Trzymamy $y$ naprawiono i włączono $x$. Kiedy$\text{I}(N,0,y)$ mamy $0 < y \lor \text{I}(N,0,y)$ dla wszystkich $y$, co potwierdza przypadek podstawowy. Następnie załóżmy, że twierdzenie to obowiązuje$x$; teraz chcemy udowodnić to twierdzenie$S(x)$. Z trichotomii dla$x$istnieją trzy przypadki: $x<y,\text{I}(N,x,y)$, i $x>y$. Gdyby$x>y$, więc wyraźnie $S(x) >y$. Gdyby$\text{I}(N,x,y)$, następnie $S(x) >y$ (tak jak $S(x) >x$ dla wszystkich $x\in \mathbb{N}$). Wreszcie załóżmy$x <y$ Następnie twierdzenie A mamy $S(x) < y$ lub $\text{I}(N,S(x),y)$, w obu przypadkach skończymy.

Twierdzenia, które chcę udowodnić, można wyrazić w Coq w następujący sposób.

Lemma less_lem (xy: N): mniej x (sucy y) -> lub (mniej xy) (IN xy).

Twierdzenie Ntrikotomia: (dla wszystkich xy: N lub (mniej xy) (lub (IN xy) (mniej yx))).

Przydatne wyniki

Tutaj zebrałem niektóre wyniki, które zdefiniowałem i do tej pory udowodniłem. To są te, o których mówię powyżej. * To jest kod, który udało mi się napisać do tej pory, zauważ, że większość składa się z definicji. *

(* Sigma types *)


Inductive Sigma (A:Set)(B:A -> Set) :Set :=
  Spair: forall a:A, forall b : B a,Sigma A B.

Definition E (A:Set)(B:A -> Set)
  (C: Sigma A B -> Set)
  (c: Sigma A B)
  (d: (forall x:A, forall y:B x, 
      C (Spair A B x y))): C c :=

match c as c0 return (C c0) with
| Spair a b => d a b
end. 


(* Binary sum type *)

Inductive sum' (A B:Set):Set := 
inl': A -> sum' A B | inr': B -> sum' A B.

Print sum'_rect.

Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=

match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.

(* Three useful finite sets *)

Inductive N_0: Set :=.

Definition R_0
  (C:N_0 -> Set)
  (c: N_0): C c :=
match c as c0 return (C c0) with
end.

Inductive N_1: Set := zero_1:N_1.

Definition R_1 
  (C:N_1 -> Set)
  (c: N_1)
  (d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
  | zero_1 => d_zero
end.

Inductive N_2: Set := zero_2:N_2 | one_2:N_2.

Definition R_2 
  (C:N_2 -> Set)
  (c: N_2)
  (d_zero: C zero_2)
  (d_one: C one_2): C c :=
match c as c0 return (C c0) with
  | zero_2 => d_zero
  | one_2  => d_one
end.


(* Natural numbers *)

Inductive N:Set :=
zero: N | succ : N -> N.

Print N. 

Print N_rect.

Definition R 
  (C:N -> Set)
  (d: C zero)
  (e: (forall x:N, C x -> C (succ x))):
  (forall n:N, C n) :=
fix F (n: N): C n :=
  match n as n0 return (C n0) with
  | zero => d
  | succ n0 => e n0 (F n0)
  end.

(* Boolean to truth-value converter *)

Definition Tr (c:N_2) : Set :=
match c as c0 with
  | zero_2 => N_0
  | one_2 => N_1
end.

(* Identity type *)

Inductive I (A: Set)(x: A) : A -> Set :=
r :  I A x x.

Print I_rect.

Theorem J 
  (A:Set)
  (C: (forall x y:A, 
              forall z: I A x y, Set))
  (d: (forall x:A, C x x (r A x)))
  (a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.

(* functions are extensional wrt
  identity types *)

Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.


(* addition *)

Definition add (m n:N) : N 
 := R (fun z=> N) m (fun x y => succ y) n.

(* multiplication *)

Definition mul (m n:N) : N 
 := R (fun z=> N) zero (fun x y => add y m) n.


(* Axioms of Peano verified *)

Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
  by applying reflexivity *)
apply r.
Defined.


Theorem P1b: (forall x y: N, 
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.


Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.


Theorem P2b: (forall x y: N, 
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.

Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.

(* alternatively
Definition pd (x: N): N :=
match x as x0 with
  | zero => zero
  | succ n0 => n0
end.
*)

Theorem P3: (forall x y:N, 
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.

Definition not (A:Set): Set:= (A -> N_0).

Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.


Theorem P4 : (forall x:N, 
not (I N (succ x) zero)).
intro x.
intro p.

apply (J N (fun x y z => 
    Tr (isnonzero x) -> Tr (isnonzero y))
    (fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.

Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
   -> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.

(* I(A,-,-) is an equivalence relation *)

Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.

Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.

Lemma Itransitive (A:Set): 
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.


Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).
intros m n H.
induction H.
apply r.
Defined.

Lemma zeroadd: (forall n:N, I N (add zero n) n).
intro n.
induction n.
simpl.
apply r.
apply succ_cong.
auto.

Defined.

Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).
intros.
induction n.
simpl.
apply r.
simpl.
apply succ_cong.
auto.

Defined.

Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).
intros n m; elim n.
apply zeroadd.
intros y H; elim (succadd m y).
simpl.
rewrite succadd.
apply succ_cong.
assumption.


Defined.

Lemma associative_add: (forall m n k:N, 
I N (add (add m n) k) (add m (add n k))).
intros m n k.
induction k.
simpl.
apply Ireflexive.
simpl.
apply succ_cong.
assumption.
Defined.

Definition or (A B : Set):= sum' A B.


Definition less (m n: N) :=
 Sigma N (fun z => I N (add m (succ z)) n).



Lemma less_lem (x y:N) : 
less x (succ y) -> or (less x y) (I N x y).
intro.
destruct H.
right.

(* Here is where I'm working right now *)

Defined.


Theorem Ntrichotomy: (forall x y:N, 
or (less x y) (or (I N x y) (less y x))).

Coq jest nieco bardziej okrutny niż papierowe dowody: kiedy piszesz „a skończyliśmy” lub „wyraźnie” w papierowym dowodzie, często można zrobić znacznie więcej, aby przekonać Coq.

Teraz trochę wyczyściłem twój kod, starając się zachować go w tym samym duchu. Możesz go znaleźć tutaj .

Kilka uwag:

1. Użyłem wbudowanych typów danych i definicji, w których myślałem, że nie zaszkodzi to twoim zamiarom. Zauważ, że gdybym użył wbudowanej równości zamiast identityi wbudowanej relacji „mniej niż”, dowody byłyby znacznie łatwiejsze, ponieważ wiele twoich lematów znajduje się w bazie danych znanych twierdzeń, które są sprawdzane przy każdym wywołaniu

   auto with arith.
   

2. Użyłem pewnych taktyk, o których prawdopodobnie nie wiesz, ale „prawdziwy” superużytkownik Coq miałby pod ręką znacznie mocniejsze taktyki i napisał własne taktyki, aby uprościć zadanie. Zawsze polecam CPDT jako miejsce, w którym można dowiedzieć się, jak stosować taktykę w potężny sposób.

3. Użyłem notacji i tabulacji, aby poprawić czytelność, oraz wbudowanych konstrukcji, takich jak dopasowywanie i inductiontaktyka, aby ułatwić sprawdzanie i ponowne uwzględnianie czynników. W szczególności twoja definicja lessbyła trudna w użyciu, możesz zobaczyć, jak ją nieco zmodyfikowałem

   $$\exists x,\ m + (x+1) = n$$ do ekwiwalentu (ale łatwiejszy w użyciu) $$\exists x,\ (x + m)+1 = n$$ tego rodzaju „modyfikowanie definicji” zdarza się często w formalnych dowodach.

4. Chociaż możesz tutaj uzyskać odpowiedzi na tego rodzaju pytania, zdecydowanie zalecamy przesłanie swojej pracy do Coq-Club, który został stworzony wyłącznie w celu udzielenia odpowiedzi na tego rodzaju pytania.

Odpowiedź Cody'ego jest doskonała i spełnia twoje pytanie dotyczące tłumaczenia twojego dowodu na Coq. Jako uzupełnienie tego chciałem dodać te same wyniki, ale udowodniłem, że używam innej trasy, głównie jako ilustrację niektórych bitów Coq i aby zademonstrować to, co możesz syntaktycznie wykazać przy bardzo niewielkiej dodatkowej pracy. Nie oznacza to jednak, że jest to najkrótsza droga - po prostu inna. Dowody zawierają tylko jeden dodatkowy lemat pomocniczy i opierają się tylko na podstawowych definicjach, nie wprowadzam dodawania, mnożenia ani żadnej z ich właściwości, ani funkcjonalnej ekstensywności, a jedyne aksjomaty Peano są prostą formą <= b -> a + c <= b + cw lemacie pomocnika (tylko dla c = 1) i indukcji strukturalnej, która i tak zawiera typy indukcyjne za darmo.

Podobnie jak Cody, gdzie myślałem, że to nie ma znaczenia, użyłem predefiniowanych typów itp., Więc przed dowodem opiszę te:

• Użyłem wbudowanego typu nat dla liczb naturalnych, który ma (do dokładnego nazewnictwa) taką samą definicję jak twoja:

Indukcyjny nat: Set: = O: nat | S: nat -> nat

• Użyłem wbudowanego pliku i lt odpowiednio dla wartości mniejszej lub równej i mniejszej niż, które mają notacyjne skróty „<=” i „<” dla czytelności. Są one zdefiniowane:

Indukcyjny le: nat -> nat -> Prop: =
| le_n: forall n, le nn
| le_S: forall nm, (le nm) -> (le n (S m)).

i

Definicja lt (nm: nat): = le (S n) m.

• Wbudowane równanie (skrót „=”) jest równością składniową i działa tak samo jak twoje „ja”, z jednym konstruktorem, który mówi, że wszystko jest równe sobie. Symetryczne i przechodnie właściwości są łatwymi dowodami stamtąd, ale w tym przypadku nie będziemy ich potrzebować. Poniższa definicja równania ma wbudowany zapis.

Indukcyjny eq (A: Type) (x: A): A -> Prop: = eq_refl: x = x

• Na koniec użyłem zdania lub (skrót „\ /” - który jest odwrotnym ukośnikiem), który ma dwa konstruktory, w zasadzie albo masz dowód na lewy argument, albo na prawy argument. Coq ma również kilka skrótowych taktyk, lewą i prawą, co oznacza po prostu odpowiednio „zastosuj or_introl” i „zastosuj or_intror”.

Indukcyjny lub (AB: Prop): Prop: =
or_introl: A -> A / B | lub_intror: B -> A / B

Teraz są moje dowody, w zasadzie, jeśli znaczniki nie przeszkadzają, powinieneś być w stanie po prostu wyciąć i wkleić to do pliku .v Coq i zadziała. Dodałem komentarze, aby zauważyć interesujące bity, ale są one w ogranicznikach (* *), więc nie powinieneś ich usuwać.

Theorem lt_or_eq: forall (n m : nat),
  n < S m -> n < m \/ n = m.
Proof.
(*
  This proof is just a case analysis on n and m, whether they're zero or
  a successor of something.
*)
destruct n as [|n']; destruct m as [|m']. 

(*n = 0, m = 0*)
intros.
  right. reflexivity.

(*n = 0, m = S m'*)
intros H.
  inversion H.
  inversion H1.
  left. unfold lt. constructor.
  (*The constructor tactic tries to match the goal to a constructor
    that's in the environment.*) 
  left. unfold lt. constructor. assumption.
  (*Assumption tries to match the goal to something that's in the
    current context*)

(*n = S n', m = 0
  This case is false, so we can invert our way out of it.*)
intros.
  inversion H. inversion H1.

(*n = S n', m = S m'*)
intros.
  inversion H.
    right. reflexivity.
    left. unfold lt. assumption.
Qed.


(*
  The following lemma with be useful in the proof of the trichotomy theorem,
  it's pretty obviously true, and easy to prove. The interesting part for
  anyone relatively new to Coq is that the induction is done on the
  hypothesis "a <= b", rather than on either a or b.
*)
Lemma a_le_b_implies_Sa_le_Sb: forall a b, a <= b -> S a <= S b.
Proof.
  intros a b Hyp.
  induction Hyp.
  constructor.
  constructor.
  apply IHHyp.
Qed.

(*
  The proof of the trichotomy theorem is a little more involved than the
  last one but again we don't use anything particularly tricky. 
  Other than the helper lemma above, we don't use anything other than the
  definitions.

  The proof proceeds by induction on n, then induction on m.  My personal
  feeling is that this can probably be shortened.  
*)
Theorem trich: forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  induction n.
    induction m.
      right. left. reflexivity.
        inversion IHm.
          left. unfold lt. constructor. unfold lt in H. assumption.
          inversion H.
          left. unfold lt. subst. constructor.
          inversion H0.     
    induction m.
      assert (n < 0 \/ n = 0 \/ 0 < n).
      apply IHn.
      inversion H.
      inversion H0.
      inversion H0.
      right. right. subst. unfold lt. constructor.
      right. right. unfold lt. constructor. assumption.
      inversion IHm. unfold lt in H.
      left. unfold lt. constructor. assumption.
      inversion H; subst.
      left. unfold lt. constructor.
      inversion H0.
      right. left. reflexivity.
      right. right. apply lt_or_eq in H0.

      inversion H0.
      apply a_le_b_implies_Sa_le_Sb. assumption.
      subst. unfold lt. apply a_le_b_implies_Sa_le_Sb. assumption.
Qed.

(*
  The following is just to show what can be done with some of the tactics
  The omega tactic implements a Pressburger arithmetic solver, so anything
  with natural numbers, plus, multiplication by constants, and basic logic
  can just be solved. Not very interesting for practicing Coq, but cool to
  know.
*)

Require Import Omega.

Example trich' : forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  intros.
  omega.
Qed.