mathcomp analysisのtopology.vにおいて,
...
Module PropInFilter : PropInFilterSig.
Definition t := prop_in_filter_proj.
...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...
mathcomp analysisのtopology.vにおいて,
...
Module PropInFilter : PropInFilterSig.
Definition t := prop_in_filter_proj.
...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...
From mathcomp Require Import all_ssreflect. | |
Require Import JMeq. | |
Inductive sizseq (T:Type) : nat -> Type := | |
| SizNil : sizseq T 0 | |
| SizCons n : T -> sizseq T n -> sizseq T n.+1. | |
Lemma sizseq0nil_aux (T:Type) n : forall xs : sizseq T n, n = 0 -> JMeq xs (SizNil T). | |
Proof. |
From mathcomp Require Import all_ssreflect. | |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Unset Printing Implicit Defensive. | |
(* :> を複数持つと予期せぬことがおきることがあるぞ *) | |
Structure S : Type := MakeS { | |
sort2 :> Type; | |
sort :> Type; |
From mathcomp Require Import all_ssreflect. | |
Fixpoint evivn_rec pred_d m q := | |
if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m). | |
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m). | |
Lemma edivn_recP1 q r m pred_d q0: | |
(q, r) = edivn_rec pred_d m q0 -> | |
r < pred_d.+1. |
Require Import String List. | |
Import ListNotations. | |
Open Scope string_scope. | |
Definition aaa := 1+2. | |
Definition bbb := aaa * 5. | |
Definition foo x y:= 2*x + y. | |
Compute foo 1 2. |
Require Import Arith Unicode.Utf8. | |
Definition f (n : nat) := | |
n - 1. | |
Inductive reaches_1 : nat → Prop := | |
| term_done : reaches_1 1 | |
| term_more (n : nat) : reaches_1 (f n) → reaches_1 n. | |
Check reaches_1_ind. |
Require Import Arith. | |
Lemma test_000: forall a b c : nat, a + b + c = b + c + a. | |
Proof. | |
intros a b c. now rewrite (Nat.add_comm a b), Nat.add_shuffle0. | |
Qed. | |
Lemma test_001: forall m : nat, 2 ^ (S m) = 2 * 2 ^ m. | |
Proof. reflexivity. Qed. |
From mathcomp Require Import ssreflect ssrnat div. | |
Lemma test_000: forall a b c : nat, a + b + c = b + c + a. | |
Proof. | |
move=> a b c. | |
rewrite (_: b + c = c + b). | |
- by apply addnCAC. | |
- by apply addnC. | |
Qed. |
Theorem contrapositive_bool : forall (p q : bool), | |
(p = true -> q = true) -> (q = false -> p = false). | |
Proof. | |
intros p q H Hq. | |
destruct p. (* pで場合分け*) | |
- (* pがtrueのとき *) | |
rewrite H in Hq. | |
+ discriminate Hq. | |
+ reflexivity. | |
- (* pがfalseのとき*) |