Section experiment Inductive state Type s1 state s2 state Fixpoint tra

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
Section experiment.
Inductive state : Type :=
| s1 : state
| s2 : state.
Fixpoint transitions(s:state):state :=
match s with
| s1 => s2
| s2 => s2
end.
Eval compute in (transitions s1).
Example test_transitions:
(transitions (transitions s1)) = s2.
Proof. simpl. reflexivity. Qed.
Fixpoint ntrans (n:nat) (s:state) :=
match n with
| 0 => s
| S n' => ntrans n' (transitions s)
end.
Lemma ntrans_const: forall n s, n>0 -> ntrans n s = s2.
Proof.
intuition.
Qed.
End experiment.