← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/output/PrintAssumptions.v

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/output/PrintAssumptions.v
 
1
 
 
2
(** Print Assumption and opaque modules :
 
3
 
 
4
  Print Assumption used to consider as axioms the modular fields
 
5
  unexported by their signature, cf bug report #2186. This should
 
6
  now be fixed, let's test this here. *)
 
7
 
 
8
(* First, a minimal test-case *)
 
9
 
 
10
Axiom foo : nat.
 
11
 
 
12
Module Type T.
 
13
 Parameter bar : nat.
 
14
End T.
 
15
 
 
16
Module M : T.
 
17
  Module Hide. (* An entire sub-module could be hidden *)
 
18
  Definition x := foo.
 
19
  End Hide.
 
20
  Definition bar := Hide.x.
 
21
End M.
 
22
 
 
23
Module N (X:T) : T.
 
24
  Definition y := X.bar. (* A non-exported field *)
 
25
  Definition bar := y.
 
26
End N.
 
27
 
 
28
Module P := N M.
 
29
 
 
30
Print Assumptions M.bar. (* Should answer: foo *)
 
31
Print Assumptions P.bar. (* Should answer: foo *)
 
32
 
 
33
 
 
34
(* The original test-case of the bug-report *)
 
35
 
 
36
Require Import Arith.
 
37
 
 
38
Axiom extensionality : forall P Q (f g:P -> Q),
 
39
  (forall x, f x = g x) -> f = g.
 
40
 
 
41
Module Type ADD_COMM_EXT.
 
42
  Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
 
43
End ADD_COMM_EXT.
 
44
 
 
45
Module AddCommExt_Opaque : ADD_COMM_EXT.
 
46
  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
 
47
  Proof.
 
48
    intro n; apply extensionality; auto with arith.
 
49
  Qed.
 
50
End AddCommExt_Opaque.
 
51
 
 
52
Module AddCommExt_Transparent <: ADD_COMM_EXT.
 
53
  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
 
54
  Proof.
 
55
    intro n; apply extensionality; auto with arith.
 
56
  Qed.
 
57
End AddCommExt_Transparent.
 
58
 
 
59
Print Assumptions AddCommExt_Opaque.add_comm_ext.
 
60
(* Should answer: extensionality *)
 
61
 
 
62
Print Assumptions AddCommExt_Transparent.add_comm_ext.
 
63
(* Should answer: extensionality *)
 
64
 
 
65
Lemma add1_comm_ext_opaque :
 
66
  (fun x => x + 1) = (fun x => 1 + x).
 
67
Proof (AddCommExt_Opaque.add_comm_ext 1).
 
68
 
 
69
Lemma add1_comm_ext_transparent :
 
70
  (fun x => x + 1) = (fun x => 1 + x).
 
71
Proof (AddCommExt_Transparent.add_comm_ext 1).
 
72
 
 
73
Print Assumptions add1_comm_ext_opaque.
 
74
(* Should answer: extensionality *)
 
75
 
 
76
Print Assumptions add1_comm_ext_transparent.
 
77
(* Should answer: extensionality *)
 
78
 
 
79
Module Type FALSE_POSITIVE.
 
80
  Axiom add_comm : forall n x, x + n = n + x.
 
81
End FALSE_POSITIVE.
 
82
 
 
83
Module false_positive : FALSE_POSITIVE.
 
84
  Lemma add_comm : forall n x, x + n = n + x.
 
85
  Proof. auto with arith. Qed.
 
86
 
 
87
  Print Assumptions add_comm.
 
88
  (* Should answer : Closed under the global context *)
 
89
End false_positive.
 
90
 
 
91
Lemma comm_plus5 : forall x,
 
92
  x + 5 = 5 + x.
 
93
Proof (false_positive.add_comm 5).
 
94
 
 
95
Print Assumptions comm_plus5.
 
96
(* Should answer : Closed under the global context *)