勉強会とかするなら参加したいわ 0095片山博文MZ ◆T6xkBnTXz7B0 2015/02/11(水) 07:12:51.62ID:Dr+1DDR1 数学の体系は、公理系によって成り立っている。すなわち、 当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、 さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。 そのように数学は、間違いのない証明によって次々と築き上げるものである。 0096片山博文MZ ◆T6xkBnTXz7B0 2015/02/11(水) 07:20:21.76ID:Dr+1DDR1 証明に1つでも間違いがあれば、公理系は崩壊する。間違いが1つでも紛れ込めば、 どんな命題でも証明可能になり、証明が無意味となる。 0097132人目の素数さん2015/02/11(水) 07:36:02.60ID:v8Hqr9Iu なにかの新書のキャッチコピーか? 0098132人目の素数さん2015/02/11(水) 09:29:50.38ID:j/Krena0>>95>>96 なにを言いたい? なお、証明が間違っていても公理系は崩壊しないw 0099132人目の素数さん2015/02/11(水) 10:23:15.61ID:dm165ELq スレ主に正直ガッカリ感 この船頭では… 0100片山博文MZ ◆T6xkBnTXz7B0 2015/02/11(水) 10:48:45.59ID:Dr+1DDR1>>98 公理の集合のことを公理系って言うんだったね。 よって>>95-96は間違い。 0101132人目の素数さん2015/02/11(水) 14:50:41.92ID:YQf1vLE3 スレ主の精神が崩壊 0102132人目の素数さん2015/02/11(水) 16:30:07.99ID:cuKCaaA+>>860103132人目の素数さん2015/02/11(水) 20:46:57.00ID:H06TaWd8>>101 それは前から分かっていること 0104片山博文MZ ◆T6xkBnTXz7B0 2015/02/13(金) 02:36:25.72ID:4T+ZQiA6 同値変換だけで命題論理式を最も単純な節形式にするって未解決だよな? 0105片山博文MZ ◆T6xkBnTXz7B0 2015/02/13(金) 13:45:35.78ID:Zi/5tAa8 クワイン・マクラスキー法 http://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%AF%E3%82%A4%E3%83%B3%E3%83%BB%E3%83%9E%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%AD%E3%83%BC%E6%B3%950106片山博文MZ ◆T6xkBnTXz7B0 2015/02/13(金) 17:47:55.74ID:4T+ZQiA6 NP困難なんて気合いと悪運で突破する! 0107132人目の素数さん2015/02/13(金) 20:56:57.57ID:Wb77hhv6 せめて近似で突破して 0108132人目の素数さん2015/02/16(月) 06:52:55.96ID:eGQOGV7p 私、O'Camlなどでのプログラミング経験はあるが数学の力に自信がないもので、数学書を一人で読み進める時にきちんと証明出来ている確信が欲しくて久しぶりにCoqを触り始めました。 証明のコードを生成してみるのもまた愉し。 0109132人目の素数さん2015/02/16(月) 11:44:48.02ID:OK+Cd/WQ>>86もう無理でしょうか。しくしく。 0110132人目の素数さん2015/02/16(月) 19:45:39.73ID:46V2KXPR Coqってグッドスタイン数列の収束は証明できるの? 0111132人目の素数さん2015/03/17(火) 05:27:20.77ID:SwDWqZM9 検証はイメージできるけど証明か 0112132人目の素数さん2015/03/17(火) 11:09:06.79ID:p3znTvh+ 検証と証明ってどう違うの 一例の場合か全ての場合かってこと? 0113132人目の素数さん2015/03/17(火) 12:42:17.91ID:SwDWqZM9 具体的に人間が与えた証明が正しい推論になっているか確かめるのが検証。 証明システムなら人工知能が結論までの道筋を自ら見つけるということになるはず。 0114132人目の素数さん2015/03/17(火) 21:53:44.21ID:sQPcb9ll Coqって順序数扱えんの? 0115132人目の素数さん2015/03/19(木) 15:02:35.75ID:g9YALw9l Variable A:Type. Variable B:(A -> Type) -> A -> Type. Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x. Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x). での Theorem r1:forall (x:A), B mu x -> mu x. の証明なんだけど、 2 subgoals A : Type B : (A -> Type) -> A -> Type m : forall P Q : A -> Type, (forall x : A, P x -> Q x) -> forall x : A, B P x -> B Q x x : A a : B mu x P : A -> Type b : forall y : A, B P y -> P y x0 : A y : mu x0 ============================ forall y0 : A, B (fun x1 : A => P x1) y0 -> P y0 subgoal 2 is: B mu x のあとどうすればいいでしょうか?上記のsubgoalの中の (fun x1 : A => P x1)をPに変える命令とかあるんでしょうか? 0116追加2015/03/19(木) 15:03:19.56ID:g9YALw9l ちなみに、 Proof. intros x a. unfold mu. intros P b. apply b. apply (m mu P). intros x0 y. apply y. までが上記の結果です。 0117132人目の素数さん2015/03/23(月) 21:55:09.34ID:hFhIEEUk>>95 >数学の体系は、公理系によって成り立っている。すなわち、 >当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、 >さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。 >そのように数学は、間違いのない証明によって次々と築き上げるものである。
ゲーデルの不完全性定理によれば あんたの言ってる事は数学の本性の上っ面でしかない 0118132人目の素数さん2015/04/13(月) 14:47:42.65ID:gEnxmz80 ここは死んでしまったのでしょうか。しくしく。 0119片山博文MZ ◆T6xkBnTXz7B0 2015/04/13(月) 16:42:48.12ID:oOocMLFA すまね。仕事で忙しい、疲れてるときは数学ができない。 0120132人目の素数さん2015/04/13(月) 19:17:53.26ID:SKfHu0g2 景気いいの? 浦山 0121132人目の素数さん2015/04/17(金) 21:21:52.45ID:oyQOgKjs>>116 Proof. intros x a. unfold mu. intros P b. apply b. apply (m mu P). intros x0 y. apply y. intro y0. apply (b y0). apply a. Qed. 0122132人目の素数さん2015/04/17(金) 22:20:53.23ID:KzUa3HIJ ((p∧q)→r)→((p→r)∨(q→r)) は証明できますか 0123132人目の素数さん2015/04/18(土) 09:18:54.32ID:Q1uVLxMU 直観主義では証明できないので Require Import Classical. Variable (p q r:Prop). Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)). Proof. apply NNPP. intuition. Qed.
Variable (p q r:Prop). Hypothesis EM_p: p\/~p. Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)). Proof. intro H. elim EM_p. intro H0. apply or_intror. intro H1. apply H. apply conj. exact H0. exact H1. intro H2. apply or_introl. intro H3. absurd p. exact H2. exact H3. Qed. 01261152015/04/18(土) 16:08:27.46ID:Ch74qrhJ>>121 レス大感謝です。しかし、 apply (b y0). のところで、 Error: Impossible to unify "B P y0 -> P y0" with "B (fun x0 : A => P x0) y0 -> P y0". と叱られました。Coqのバージョンが Welcome to Coq 8.3pl3 で古いのでしょうか。 01271222015/04/18(土) 18:57:48.32ID:CUF6Decr>>123-125 ありがとうございます。 知らなったタクティクがいっぱいありますね。 0128132人目の素数さん2015/04/19(日) 20:01:47.33ID:wQv7TFhy>>126 coq8.4からη変換が入ったみたいね 多分これでη変換無しで行けると思う
Variable A:Type. Variable B:(A -> Type) -> A -> Type. Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x. Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).
Theorem r1:forall (x:A), B mu x -> mu x. Proof. intros x a. unfold mu. intros P b. apply b. apply (m mu P). intros x0 y. apply y.
intros y0 c. apply b. apply (m (fun x : A => P x) P). trivial. exact c. exact a. Qed. 01291152015/04/21(火) 16:23:18.95ID:X1phHP6G>>128 レス大感謝です。さて、また私にとって難題です。エラーが出る最小限の 手順を用意しましたので、偉い方、どうかお付き合いください。 第1の例 Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b. Proof. intros a b Hab. assert (Hta:(a = b) /\ (b = a)). apply Ee. unfold Eqt. assumption.(*ここでエラーが出ます*) Qed.
これは、Display implicit argumentsとDeactivate notations display をすることによって、Implicitな変数が原因であることがわかりました。 01301292015/04/21(火) 16:25:47.49ID:X1phHP6G そこで、次のように証明手順を変えてみると、なんと、最期のassumptionで Proof completed.が表示されるのに、Qedの後エラーとなるのです。 第2の例 Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b. Proof. intros a b Hab. assert (Hta:(a = b) /\ (b = a)). apply Ee in Hab. assumption. elim Hta. intros H H0. assumption. Qed.
どうかお救いください。トホホ 0131132人目の素数さん2015/04/24(金) 23:44:49.27ID:RQUiSeMS @eq Set a b と @eq Type a b は違う型なのが原因な気がする。 130のようなQedでエラーになるのは結構あって、証明モードの途中ではあんまり頑張って型検査しないから、 こういう微妙な型の差しかないときはしかたないかな。 01321292015/04/29(水) 09:13:55.74ID:Z8S8LZWA レス大感謝です。結局は反則をすることによって解決しました。つまり、 証明法を探すのではなく、>>129の >Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A). の部分を Definition Eqt (T:Type) (A B:T) : Prop := (eq (A := T) A B) \/ (eq (A := T) B A). Implicit Arguments Eqt [T]. と変えました。これで、>>129の証明の仕方でもエラーは出なくなりました。 ちなみに最期まで証明すると、 Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C):= fun A B C a b c => ?. 0222132人目の素数さん2021/06/13(日) 12:05:53.03ID:lCrOJ5I2>>221 Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) := fun A B C f b a => f a b. かな。f の型が (A -> B -> C) で、b の型が B で、a の型が A 。 「ならば」(->) は右結合だから、(B -> A -> C) の部分の括弧は外す事ができる。 0223132人目の素数さん2021/06/17(木) 19:16:48.45ID:oqo44TQm 証明支援システムCoq、新しい名称を検討中 https://developers.srad.jp/story/21/06/16/1737205/0224132人目の素数さん2022/01/12(水) 08:10:41.00ID:0y6QDPS2 コックむずい 0225132人目の素数さん2022/01/24(月) 07:16:51.96ID:OmUr/Vw+ ムズいよねえ もっと勉強しなくては 0226132人目の素数さん2022/02/11(金) 01:30:20.50ID:92XxvpJY | \ |Д`) ダレモイナイ・・オドルナラ イマノウチ |⊂ |
以下だと分かりやすいかも Lemma f_test :forall A:Prop, A -> not A -> True. Proof. intros H H0 H1. apply H1 in H0. case H0. Qed. 0273132人目の素数さん2023/03/16(木) 22:10:00.35ID:/qOR2FZK>>272