File: bug_4596.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (15 lines) | stat: -rw-r--r-- 425 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.

Definition T (x : bool) := x = true.

Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat)
  (s : forall n : nat, bool)
  (s0 s1 : nat -> S -> S),
  (forall (str0 : S) (n m : nat),
  (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) ->
    T (b str0 m)) ->
  T (b str p).
Proof.
intros ???????? H0.
rewrite H0.
Abort.