Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(*** Logical propositions ***) Require Import ZArith. Open Scope Z_scope. Open Scope bool_scope. Check 2 = 2. Check 2 = 3. Check negb (negb true) = true. Check Zlt. Check Zlt 2 3. Check le. Check le 0%nat 6%nat. Check 2 < 3. Check 2 > 3. Check 2 = 3. Check Zeq_bool 2 3. Check Zlt_bool 2 3. Definition Zmax n p := if Zlt_bool n p then p else n. (* Definition Zmax' n p := if n < p then p else n. *) Check Zlt_bool 2 3 = true. (* quantifiers connectives *) Check forall n:Z, 0 <= n * n. Check exists n:Z, n * n = 4. Check forall n:Z, 0 <= n \/ n < 0. Check forall n p : Z, n < p \/ p <= n. Check forall n : Z, n ^ 2 <= 2 ^ n. Check Zlt_irrefl. Check forall n : Z, ~ n < n. Check ~ exists n:Z, n*n = 2. SearchPattern (~(_<_)). Check forall n m : Z, n < m -> ~ m < n. Check forall n:Z, exists p:Z, p < n. Check forall n m p:Z, n <= m -> m <= p -> n <= p. Check forall n p:Z, n < p \/ n = p \/ p < n. Locate Zle_bool. Check let (q,r) := Zdiv_eucl 456 37 in 456 = 37 * q + r /\ 0 <= r < 37. Check forall a b q r: Z, 0 < b -> a = b * q + r -> 0 <= r < b -> q = a / b /\ r = a mod b. Check (forall n : nat, n = 0 \/ exists p:nat, p < n)%nat. (** Names and theorems *) Check Zle_trans. Definition Z_unbounded := ~ exists n:Z, forall p:Z, p <= n. Check Z_unbounded. Print Z_unbounded. Check exists z:Z, forall n:Z, z+n=n. Definition neutral (z:Z) := forall n:Z, z+n=n. Check exists z:Z, neutral z. Check exists z:Z, neutral z /\ forall z', neutral z' -> z' = z. SearchPattern (~ (_ < _)). Check (Zlt_irrefl 23). Check (Zle_trans 4 7 8). (**** More examples ***) Require Import List. SearchAbout [In app]. Check forall l:list Z, l = nil \/ exists a, exists l', l = a::l'. Check (In 3 (2::3::4::5::nil)). Check forall l1 l2 : list Z, (forall z:Z, In z (l1 ++ l2) <-> In z l1 \/ In z l2). Check forall z:Z, ~ In z nil. Definition is_square_root (n r : Z) := r * r <= n < (r+1)*(r+1). Check is_square_root 9 3. Definition is_prime (n:Z) := 2 <= n /\ forall p q, 0 < p -> 0 < q -> n = p * q -> p = n \/ q = n. Parameter sorted_Zle : list Z -> Prop. Check sorted_Zle (2::3::4::5::nil). Fixpoint nb_occ (n:Z)(l:list Z) : nat := match l with nil => 0%nat | a::l' => if Zeq_bool n a then S(nb_occ n l') else nb_occ n l' end. Check forall n l l', nb_occ n (l++l')= (nb_occ n l + nb_occ n l')%nat. Definition is_perm (l l':list Z) := forall n, nb_occ n l = nb_occ n l'. Definition preserves_occurrences (m : list Z -> list Z -> list Z) := forall l l' n, nb_occ n (m l l')= (nb_occ n l + nb_occ n l')%nat. Definition preserves_sort (m : list Z -> list Z -> list Z) := forall l l', sorted_Zle l -> sorted_Zle l' -> sorted_Zle (m l l'). Definition merge_spec (m : list Z -> list Z -> list Z):= preserves_sort m /\ preserves_occurrences m. Definition log10_spec (l:Z -> Z) := forall n p, 0 <= p -> 10 ^ p <= n < 10^(p+1)-> l n = p. (*** Some relations between boolean functions and predicates *) Require Import "Tools". Open Scope Z_scope. Check Zle_false_e. Check Zle_bool_imp_le. SearchAbout [Zle_bool Zle]. (*** Quantifying over propositions and predicates *) Check forall P : Prop, ~ P <-> (P -> False). Check forall P Q : Prop, ~ (P \/ Q) -> ~ P /\ ~ Q. Check forall P Q, P \/ Q -> Q \/ P. Check absurd. Check forall P : nat -> Prop, ~ (exists n, P n) -> forall n, ~ P n. Definition or_ex (P Q : Prop) := P /\ ~Q \/ ~P /\ Q. Goal forall P Q, or_ex P Q -> ~(P <-> Q). unfold or_ex;tauto. Qed. (*** Quantifying over types *) SearchRewrite (rev (rev _)). Check forall (A:Type)(l : list A), rev (rev l)=l. Definition decides (A:Type)(P:A->Prop)(p : A -> bool) := forall a:A, P a <-> (p a)=true. Definition decides2 (A:Type)(P:A->A->Prop)(p : A -> A-> bool) := forall a , decides A (P a) (p a). Definition decides2' (A:Type)(P:A->A->Prop)(p : A -> A-> bool) := forall a b :A , P a b <-> p a b =true. Goal forall A (P:A->A->Prop)(p : A -> A-> bool), decides2 A P p <-> decides2' A P p. unfold decides2, decides2', decides. tauto. Qed. Lemma Zle_decide : decides2 _ Zle Zle_bool. red. intros a b. split. SearchRewrite ( Zle_bool _ _). apply Zle_imp_le_bool. SearchAbout Zle_bool. apply Zle_bool_imp_le. Qed. Goal 5 <= 8. rewrite (Zle_decide 5 8). trivial. Qed. Open Scope nat_scope. Check nat_ind. Check order. Section sort_spec. Parameter sorted : forall (A:Type), relation A -> list A -> Prop. Variable s : forall A:Type, (A->A->bool) -> list A -> list A. Definition sort_correct := forall A (R : relation A) (r : A -> A -> bool), order A R -> decides2 A R r -> forall l, let l' := s _ r l in sorted A R l' /\ forall a, In a l <-> In a l'. End sort_spec. Check sort_correct _ Zle Zle_bool. Check forall (A:Type)(P:A->Prop), ~(exists x, P x ) -> forall x, ~ P x.