diff options
Diffstat (limited to 'Algebra/Terms.lean')
| -rw-r--r-- | Algebra/Terms.lean | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean index aa853a8..997dca4 100644 --- a/Algebra/Terms.lean +++ b/Algebra/Terms.lean @@ -87,6 +87,29 @@ def TermAtDepth.bound {n : β} (a : πΈ) (f : sig.bound) (args : sig.boundArgs TermAtDepth πΈ sig X (n + sig.boundDepth f) := β¨.bound a f (Subtype.val β args), by constructor; intro arg; exact (args arg).propβ© +theorem TermAtDepth.induction + {motive : {n : β} β TermAtDepth πΈ sig X n β Prop} + (var : β (x : X), motive (.var x)) + (pure : β {n : β} (f : sig.pure) (args : sig.pureArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.pure f args)) + (free : β {n : β} (a : πΈ) (f : sig.free) (args : sig.freeArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.free a f args)) + (bound : β {n : β} (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.bound a f args)) + : β {n : β} (t : TermAtDepth πΈ sig X n), motive t := by + intro n β¨t, htβ© + induction' t generalizing n <;> cases ht <;> expose_names + Β· exact var x + Β· let args' : sig.pureArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact pure f args' args_ih' + Β· let args' : sig.freeArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact free a f args' args_ih' + Β· let args' : sig.boundArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact bound a f args' args_ih' + end ConvenienceConstructors section Substitution |